Ciro Santilli @cirosantilli 40

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:

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:
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.
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

 Read the full article

Project Euler solutions in X 2026-01-30

 Read the full article

cirosantilli/project-euler-solutions 2026-01-30

 View more

At github.com/cirosantilli/project-euler-solutions Ciro Santilli attempted to do it with LLMs.

 Read the full article

Project Euler solutions 2026-01-30

 View more

Repositories of numerical solutions:

Repositories of code solutions:

euler.stephan-brumme.com/ large number of solutions in C++, stopped around 600. Informal permissive license, e.g. at: euler.stephan-brumme.com/243/
I hope you enjoy my code and learn something - or give me feedback how I can improve my solutions.
All of my solutions can be used for any purpose and I am in no way liable for any damages caused.
You can even remove my name and claim it's yours. But then you shall burn in hell.
Asked for a more formal open license at: github.com/stbrumme/euler/issues/7
www.ivl-projecteuler.com/home 330+ solutions in Python as of 2025. Random looking problem selection. On GitHub: github.com/igorvanloo/Project-Euler-Explained under Unlicense license, a public domain license.
www.nayuki.io/page/project-euler-solutions. Large number of solutions, mostly in Java and Python primarily but also Mathematica and Haskell sometimes. Proprietary license.

Repositories with hints but no solutions:

github.com/RodericGuigoCorominas/project-euler

Basically no one has ever had the patience to create a single source that solves them all, all the above were done by individuals and stopped at some point. What we need is either a collaborative solution, or... LLMs.

 Read the full article

 Unlisted articles are being shown, click here to show only listed articles.