A collection of selected mathematical proofs, their Lean formalizations, and their written presentations.
A comparator setup is available in ComparatorChallenges/,
with a separate challenge and Comparator configuration for each proof.
Each checks its fully proved standalone Lean solution.