Skip to content

Remove open BigOperators which does nothing #218

Remove open BigOperators which does nothing

Remove open BigOperators which does nothing #218

Triggered via pull request October 21, 2024 15:43
Status Failure
Total duration 11m 35s
Artifacts

lean.yml

on: pull_request
Fit to window
Zoom out
Zoom in

Annotations

10 errors and 1 warning
Build: lean4/src/putnam_1964_a2.lean#L16
The docstring for putnam_1964_a2 is not in sync with the version in `informal/putnam.json`. Please either change this docstring or modify the JSON file. Be careful to escape LaTeX when writing JSON. The JSON file currently contains: Let $\alpha$ be a real number. Find all continuous real-valued functions $f : [0, 1] \to (0, \infty)$ such that \begin{align*} \int_0^1 f(x) dx &= 1, \\ \int_0^1 x f(x) dx &= \alpha, \\ \int_0^1 x^2 f(x) dx &= \alpha^2. \\ \end{align*} While the docstring contains: Let $\alpha$ be a real number. Find all continuous real-valued functions $f : [0, 1] \to (0, \infty)$ such that \begin{align*} \int_0^1 f(x) dx &= 1, \\ \int_0^1 x f(x) dx &= \alpha, \\ \int_0^1 x^2 f(x) dx &= \alpha^2. \\ \end{align*}
Build: lean4/src/putnam_1964_a4.lean#L12
The docstring for putnam_1964_a4 is not in sync with the version in `informal/putnam.json`. Please either change this docstring or modify the JSON file. Be careful to escape LaTeX when writing JSON. The JSON file currently contains: The sequence of integers $u_n$ is bounded and satisfies \[ u_n = \frac{u_{n-1} + u_{n-2} + u_{n-3}u_{n-4}}{u_{n-1}u_{n-2} + u_{n-3} + u_{n-4}}. \] Show that it is periodic for sufficiently large $n$. While the docstring contains: The sequence of integers $u_n$ is bounded and satisfies \[ u_n = \frac{u_{n-1} + u_{n-2} + u_{n-3}u_{n-4}}{u_{n-1}u_{n-2} + u_{n-3} + u_{n-4}}. \] Show that it is periodic for sufficiently large $n$.
Build: lean4/src/putnam_1964_a5.lean#L11
The docstring for putnam_1964_a5 is not in sync with the version in `informal/putnam.json`. Please either change this docstring or modify the JSON file. Be careful to escape LaTeX when writing JSON. The JSON file currently contains: Prove that there exists a constant $k$ such that for any sequence $a_i$ of positive numbers, \[ \sum_{n=1}^{\infty} \frac{n}{a_1 + a_2 + \dots + a_n} \leq k \sum_{n=1}^{\infty}\frac{1}{a_n}. \] While the docstring contains: Prove that there exists a constant $k$ such that for any sequence $a_i$ of positive numbers, \[ \sum_{n=1}^{\infty} \frac{n}{a_1 + a_2 + \dots + a_n} \leq k \sum_{n=1}^{\infty}\frac{1}{a_n}. \]
Build: lean4/src/putnam_1969_b6.lean#L18
The docstring for putnam_1969_b6 is not in sync with the version in `informal/putnam.json`. Please either change this docstring or modify the JSON file. Be careful to escape LaTeX when writing JSON. The JSON file currently contains: Let $A$ be a $3 \times 2$ matrix and $B$ be a $2 \times 3$ matrix such that $$AB = \begin{pmatrix} 8 & 2 & -2 \\ 2 & 5 & 4 \\ -2 & 4 & 5 \end{pmatrix}. $$ Prove that $$BA = \begin{pmatrix} 9 & 0 \\ 0 & 9 \end{pmatrix}.$$ While the docstring contains: Let $A$ be a $3 \times 2$ matrix and $B$ be a $2 \times 3$ matrix such that $$AB = \begin{pmatrix} 8 & 2 & -2 \\ 2 & 5 & 4 \\ -2 & 4 & 5 \end{pmatrix}. $$ Prove that $$BA = \begin{pmatrix} 9 & 0 \\ 0 & 9 \end{pmatrix}.$$
Build: lean4/src/putnam_1977_a6.lean#L16
The docstring for putnam_1977_a6 is not in sync with the version in `informal/putnam.json`. Please either change this docstring or modify the JSON file. Be careful to escape LaTeX when writing JSON. The JSON file currently contains: Let $X$ be the square $[0, 1] \times [0, 1]$, and let $f : X \to \mathbb{R}$ be continuous. If $\int_Y f(x, y) \, dx \, dy = 0$ for all squares $Y$ such that \begin{itemize} \item[(1)] $Y \subseteq X$, \item[(2)] $Y$ has sides parallel to those of $X$, \item[(3)] at least one of $Y$'s sides is contained in the boundary of $X$, \end{itemize} is it true that $f(x, y) = 0$ for all $x, y$? While the docstring contains: Let $X$ be the square $[0, 1] \times [0, 1]$, and let $f : X \to \mathbb{R}$ be continuous. If $\int_Y f(x, y) \, dx \, dy = 0$ for all squares $Y$ such that \begin{itemize} \item[(1)] $Y \subseteq X$, \item[(2)] $Y$ has sides parallel to those of $X$, \item[(3)] at least one of $Y$'s sides is contained in the boundary of $X$, \end{itemize} is it true that $f(x, y) = 0$ for all $x, y$?
Build: lean4/src/putnam_1978_a4.lean#L19
The docstring for putnam_1978_a4 is not in sync with the version in `informal/putnam.json`. Please either change this docstring or modify the JSON file. Be careful to escape LaTeX when writing JSON. The JSON file currently contains: A binary operation (represented by multiplication) on $S$ has the property that $(ab)(cd) = ad$ for all $a, b, c, d$. Show that: \begin{itemize} \item[(1)] if $ab = c$, then $cc = c$; \item[(2)] if $ab = c$, then $ad = cd$ for all $d$. \end{itemize} Find a set $S$, and such a binary operation, which also satisfies: \begin{itemize} \item[(A)] $a a = a$ for all $a$; \item[(B)] $ab = a \neq b$ for some $a, b$; \item[(C)] $ab \neq a$ for some $a, b$. \end{itemize} While the docstring contains: A binary operation (represented by multiplication) on $S$ has the property that $(ab)(cd) = ad$ for all $a, b, c, d$. Show that: \begin{itemize} \item[(1)] if $ab = c$, then $cc = c$; \item[(2)] if $ab = c$, then $ad = cd$ for all $d$. \end{itemize} Find a set $S$, and such a binary operation, which also satisfies: \begin{itemize} \item[(A)] $a a = a$ for all $a$; \item[(B)] $ab = a \neq b$ for some $a, b$; \item[(C)] $ab \neq a$ for some $a, b$. \end{itemize}
Build: lean4/src/putnam_1978_a5.lean#L11
The docstring for putnam_1978_a5 is not in sync with the version in `informal/putnam.json`. Please either change this docstring or modify the JSON file. Be careful to escape LaTeX when writing JSON. The JSON file currently contains: Let $a_1, a_2, \dots , a_n$ be reals in the interval $(0, \pi)$ with arithmetic mean $\mu$. Show that \[ \prod_{i=1}^n \left( \frac{\sin a_i}{a_i} \right) \leq \left( \frac{\sin \mu}{\mu} \right)^n. \] While the docstring contains: Let $a_1, a_2, \dots , a_n$ be reals in the interval $(0, \pi)$ with arithmetic mean $\mu$. Show that \[ \prod_{i=1}^n \left( \frac{\sin a_i}{a_i} \right) \leq \left( \frac{\sin \mu}{\mu} \right)^n. \]
Build: lean4/src/putnam_1978_b3.lean#L15
The docstring for putnam_1978_b3 is not in sync with the version in `informal/putnam.json`. Please either change this docstring or modify the JSON file. Be careful to escape LaTeX when writing JSON. The JSON file currently contains: The polynomials $P_n(x)$ are defined by \begin{align*} P_1(x) &= 1 + x, \\ P_2(x) &= 1 + 2x, \\ P_{2n+1}(x) &= P_{2n}(x) + (n + 1) x P_{2n-1}(x), \\ P_{2n+2}(x) &= P_{2n+1}(x) + (n + 1) x P_{2n}(x). \end{align*} Let $a_n$ be the largest real root of $P_n(x)$. Prove that $a_n$ is strictly monotonically increasing and tends to zero. While the docstring contains: The polynomials $P_n(x)$ are defined by \begin{align*} P_1(x) &= 1 + x, \\ P_2(x) &= 1 + 2x, \\ P_{2n+1}(x) &= P_{2n}(x) + (n + 1) x P_{2n-1}(x), \\ P_{2n+2}(x) &= P_{2n+1}(x) + (n + 1) x P_{2n}(x). \end{align*} Let $a_n$ be the largest real root of $P_n(x)$. Prove that $a_n$ is strictly monotonically increasing and tends to zero.
Build: lean4/src/putnam_1979_b6.lean#L11
The docstring for putnam_1979_b6 is not in sync with the version in `informal/putnam.json`. Please either change this docstring or modify the JSON file. Be careful to escape LaTeX when writing JSON. The JSON file currently contains: Let $z_i$ be complex numbers for $i = 1, 2, \dots, n$. Show that \[ \left \lvert \mathrm{Re} \, [(z_1^2 + z_2^2 + \dots + z_n^2)^{1/2} ] \right \rvert \leq \lvert \mathrm{Re} \, z_1 \rvert + \lvert \mathrm{Re} \, z_2 \rvert + \dots + \lvert \mathrm{Re} \, z_n \rvert. \] While the docstring contains: Let $z_i$ be complex numbers for $i = 1, 2, \dots, n$. Show that \[ \left \lvert \mathrm{Re} \, [(z_1^2 + z_2^2 + \dots + z_n^2)^{1/2} ] \right \rvert \leq \lvert \mathrm{Re} \, z_1 \rvert + \lvert \mathrm{Re} \, z_2 \rvert + \dots + \lvert \mathrm{Re} \, z_n \rvert. \]
Build: lean4/src/putnam_1983_a4.lean#L11
The docstring for putnam_1983_a4 is not in sync with the version in `informal/putnam.json`. Please either change this docstring or modify the JSON file. Be careful to escape LaTeX when writing JSON. The JSON file currently contains: Prove that for $m = 5 \pmod 6$, \[ \binom{m}{2} - \binom{m}{5} + \binom{m}{8} - \binom{m}{11} + ... - \binom{m}{m-6} + \binom{m}{m-3} \neq 0. \] While the docstring contains: Prove that for $m = 5 \pmod 6$, \[ \binom{m}{2} - \binom{m}{5} + \binom{m}{8} - \binom{m}{11} + ... - \binom{m}{m-6} + \binom{m}{m-3} \neq 0. \]
Build
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v3, actions/cache@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/