Job application by Ciro Santilli Created 2025-04-18 Updated 2025-11-05
2025 round one during week of April 21st, not toning down online profiles:
Keywords:
Project Euler Lean solutions Created 2026-01-30 Updated 2026-02-08
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:
Mentions:
In other proof assistants, therefore with similar beauty: