README.md

Lean 4 Playground

See it in action here.

Install Lean 4 and Configure it

Just trigger it following Quickstart in Lean 4 Manual with the help from the VSCode extension for Lean 4.

Run tests

lake test

See scripts/test for more details about running individual tests, and test options.

Minimalize a file

Check out Playground/Zulip/CodeActions.lean.

Plans

Explore the following:

• SciLean
• HepLean
• cedar-spec
• SampCert
• Lean-MLIR
• verbose-lean4
• Duper
• Games in Lean
  • lean4-maze
  • TwoFX/sudoku
  • Rubik's cubes
    • vihdzp/rubik-lean4
    • kendfrey/rubiks-cube-group
    • gshartnett/rubiks-clifford-synthesis

Maybe each needs a separate Lean 4 project so these dependencies can be upgraded separately.