ImProver: Agent-Based Automated Proof Optimization

Evaluation for miniCodeProps: a Minimal Benchmark for Proving Code Properties

Neural theorem proving evaluation via the Lean REPL

Neural theorem proving toolkit: data extraction tools for Lean 4

Evaluate your LLM's response with Prometheus and GPT4 💯

LLMs + Lean, on your laptop or in the cloud

Neural theorem proving tutorial, version II

Easy-to-Hard Generalization: Scalable Alignment Beyond Human Supervision

Simple and efficient pytorch-native transformer training and inference (batched)

Tutorial on neural theorem proving

A high-throughput and memory-efficient inference and serving engine for LLMs

A simple REPL for Lean 4, returning information about errors and sorries.

llmstep: [L]LM proofstep suggestions in Lean 4.

A simple REPL for Lean 4, returning information about errors and sorries.

An environment for learning formal mathematical reasoning from scratch

Benchmark for undergraduate-level formal mathematics

An updated version of miniF2F with lots of fixes and informal statements / solutions.

A unified benchmark for math reasoning

PyTorch + HuggingFace code for RetoMaton: "Neuro-Symbolic Language Modeling with Automaton-augmented Retrieval" (ICML 2022), including an implementation of kNN-LM and kNN-MT

An open bibliography of machine learning for formal proof papers

https://albertqjiang.github.io/Portal-to-ISAbelle/

NaturalProver: Grounded Mathematical Proof Generation with Language Models