Statements from 2025 #315
Statements from 2025 #315
Conversation
|
Now let me address the CI issues. |
|
Seems the errors are all because of missing linebreaks. Hopefully it is okay now. |
lean4/src/putnam_2025_b4.lean
Outdated
| Let $S$ be the sum of the entries of $A$, and let $N$ be the number of nonzero entries of $A$. | ||
| Prove that $S \leq \frac{(n+2)N}{3}$. | ||
| Note: We parameterize by $m$ where $n = m + 2$, so $m \geq 0$ and the matrix is $(m+2) \times (m+2)$. |
There was a problem hiding this comment.
I think this will fail CI because the Note isn't part of the informal JSON (CI checks docstring is the same). Perhaps you can move this note elsewhere?
There was a problem hiding this comment.
Sorry missed this, one. Just pushed a fix.
|
Working on a fix right now. |
|
By the way is there a way to automatically extract all the doc strings? |
I don't think we have code checking in anywhere for that unfortunately. A simple script should be able to handle this I think |
|
Just added the missing newline character in b1,b2,b3 |
|
Is the current CI failure possibly caused by some definitions are not part of the problem statement? |
|
Thank you so much for the contribution, Jujian! |
2 participants
This PR includes the problem statements from Putnam 2025