comparator

Tech stack & purpose

Comparator is a verification tool for Lean 4 proof assistants that validates whether a proposed proof solution matches a challenge specification and adheres to axiom constraints. The tool operates in the formal methods domain, ensuring that theorems in a solution file prove the same statements as those in a challenge file, use only permitted axioms, and are accepted by the Lean kernel. It is built around the Lean 4 ecosystem and relies on external binaries including `landrun` for sandboxing, `lean4export` for environment extraction, and optionally `nanoda` for additional kernel verification, with the comparator itself written in a Lean-compatible environment. Comparator was originally developed by Lean FRO with support from the AIMO team for use in trustworthy LLM evaluation on the Kaggle platform.

Languages

Contributors

• 
  Henrik Böving61 commits · 182 followers
• 
  Kim Morrison20 commits · 552 followers
• 
  Garmelon13 commits · 42 followers
• 
  Moritz Firsching6 commits · 129 followers
• Rob Simmons3 commits
• 
  Joachim Breitner3 commits · 649 followers
• 
  Sebastian Ullrich2 commits · 348 followers
• 
  Robert J. Simmons1 commits · 144 followers
• 
  Matteo Cipollina1 commits · 12 followers