= <Project Euler> <Lean> solutions
Using <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:
* https://github.com/mfornet/project-euler-lean Attempts proofs, but only did <Project Euler problem 1> :-)
* https://github.com/pcpthm/pe solved the first 50, but as stated on the README itself, no proofs, so boring
* https://unreasonableeffectiveness.com/learning-lean-4-as-a-programming-language-project-euler/ solves 4, but no proofs
Mentions:
* https://leanprover-community.github.io/archive/stream/270676-lean4/topic/Competitive.20programmers.html#287860835[Alex J. Best (Jun 29 2022 at 14:20)] on the <Lean Zulip> mentions:
> 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.
That dude was actually working at <harmonic.fun> as of 2025, bastard.
* https://codeforces.com/blog/entry/124615
In other <proof assistants>, therefore with similar beauty:
* <Coq>
* https://github.com/airobo/Project-Euler-in-Coq[]: 1 and 2 with proofs
Back to article page
