LeanDisco

Eurisko-Inspired Discovery System for Lean in Lean

Warning: this is an early exploration, which will be re-written with a more solid architecture.

Cloning

git clone --recursive https://github.com/namin/LeanDisco.git

Running

lake build builds the system. Then run each test XXX with lake lean TestXXX.lean. Test files also run interactively in VSCode Lean extension.

Domain-Specific Discovery Tests

• lake lean TestInfiniteNumbers.lean
• lake lean TestFiniteFields.lean
• lake lean TestLists.lean
• lake lean TestNumberTheory.lean
• lake lean TestGroupRing.lean

Some of these are slow and output incrementally in log directory.

Benchmark Tests

• lake lean TestBenchmarks.lean -- Full miniF2F benchmark infrastructure (0% success on hard problems)
• lake lean TestTrivialProofs.lean -- End-to-end proof that pipeline works (100% success on easy problems)
• lake lean TestSingleGoal.lean -- Diagnostic tool for testing individual theorems (configurable in file)

References

• Software Archaeology of Eurisko: a reflective port in Common Lisp, based on unearthed original file.
• llmlean: probably a good starting point to think about LLM integration from within Lean.