Ciro Santilli
OurBigBook.comUsing Lean or other programmable proof assistants to solve Project Euler is the inevitable collision of two autisms. In particular, using Lean to prove that you have the correct solution, just making a Lean program that prints out the correct solution is likely now trivial as of 2025 by asking an LLM to port a Python solution to the new language.
Some efforts:
- github.com/mfornet/project-euler-lean Attempts proofs, but only did Project Euler problem 1 :-)
- github.com/pcpthm/pe solved the first 50, but as stated on the README itself, no proofs, so boring
- unreasonableeffectiveness.com/learning-lean-4-as-a-programming-language-project-euler/ solves 4, but no proofs
Mentions:
- Alex J. Best (Jun 29 2022 at 14:20) on the Lean Zulip mentions:That dude was actually working at harmonic.fun as of 2025, bastard.
It would also be very interesting to collect verified fast Project Euler solutions for Lean 4 at some point, this would simultaneously work out the compiled speed and the mathematics libraries which would be fun.
- codeforces.com/blog/entry/124615
In other proof assistants, therefore with similar beauty:
- Coq
- github.com/airobo/Project-Euler-in-Coq: 1 and 2 with proofs