Python
2 entries
- QL-0023
Erdős Problem 357: bounds on sequences with distinct consecutive sums, formalized in Lean
For Erdős Problem 357, the largest k with 1 ≤ a₁ < … < aₖ ≤ n and all consecutive sums distinct satisfies f(n) ≤ (44273/90000)n + 2√n + 177792 and, for large n, f(n) ≥ (15/√21)√n − 1800. The proofs and the Lean formalization were produced by AI agents, and the Lean statements are pinned to the community’s formal definition. Whether f(n) = o(n) is still open.
Rev. A - QL-0021
Testing a PS2 game with no one at the controller
How the Tekken 4 project proves changes in game without a person playing: PCSX2 is booted by script, steered with synthetic key presses, and asked for savestates, which hold all 32 MB of main memory plus sound and video memory. Every in-game result in the project was produced this way, with rules learned from the times it went wrong.
Rev. A