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 16 3

2. 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

3. lean4-gym lean4-gym Public

   Forked from PatrickMassot/lean-gym

   A REPL-like interface for Lean4 tactic proofs.

   Lean 2

4. 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

5. formal-systems formal-systems Public

   This repository contains implementations of various formal systems such as lambda calculus, SKI combinatory calculus and propositional logic.

   Julia 1

6. 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 1