Stars
Hand-written verified Lean solutions for the HumanEval benchmark
CLEVER: Code Lean Evaluation for Verified End-to-end Reasoning
Canonical is a performant sound and complete type inhabitation solver for dependent type theory.
Experiments on automation for Lean
A prototype for a monadic program logic in Lean that has since been upstreamed into the Lean 4 repo
A project to digitalise results from physics into Lean.
The official repository for the paper Multilingual Mathematical Autoformalization
An updated version of miniF2F with lots of fixes and informal statements / solutions.
Intuitive, type-safe expression quotations for Lean 4.
GitHub Action for the OCaml programming language
cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.
👀 dynamically interact with vim registers
computable implementation of real numbers in Lean4
A jq clone focussed on correctness, speed, and simplicity
(Mirror) A Machine-to-Machine Interaction System for Lean 4
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
Code related to the Lean verification of the empty hexagon theorem
A deprecated equality saturation tactic for Lean based on egg.
A Machine-to-Machine Interaction System for Lean 4.
Tactics for discharging Lean goals into SMT solvers.
A Foreign Function Interface (FFI) to cvc5 solver in Lean.
A proof assistant for general type theories