Popular repositories Loading

1. lean-slides lean-slides Public

   A tool to auto-generate and render slides from Markdown comments in the Lean editor.

   Lean 25 8

2. kimina kimina Public

   A Lean tactic that invokes the Kimina Prover Preview model to offer proof suggestions.

   Lean 11 1

3. lean3-statement-translation-tool lean3-statement-translation-tool Public

   A tool for automatic formalisation of natural language theorem statements to Lean3 code using OpenAI Codex.

   Lean 7

4. combinatornithology combinatornithology Public

   A series of puzzles on combinatory logic written in LEAN, inspired by the book "To Mock a Mockingbird" by Raymond Smullyan.

   Lean 2

5. lean4-gym lean4-gym Public

   Forked from PatrickMassot/lean-gym

   A REPL-like interface for Lean4 tactic proofs.

   Lean 2

6. theorem-proving theorem-proving Public

   This repository contains code for automated proofs to (or verifications of) problems, mainly from Euclidean Geometry, using the Z3 SMT solver.

   Jupyter Notebook 1