Since July I’ve had Claude Code and Codex grinding on Erdős Problem #993 (1987, unimodality of the independent-set sequence of trees). Ran a literature check today: a complete proof was posted last week by Tong Zhang and Wei Li, and two Lean 4 formalizations already claim a clean build. Not peer-reviewed yet.
- Paper: https://doi.org/10.5281/zenodo.22999166
- Lean: https://github.com/selfreferencing/erdos993-lean and https://github.com/lixiang90/forest-unimodality
- Problem page: https://www.erdosproblems.com/993 submitted by /u/Odd-Sympathy1274
Originally posted by u/Odd-Sympathy1274 on r/ArtificialInteligence
You must log in or # to comment.