Software

Llemma models
Open language models for mathematics.
7B model. 34B model. Training data. Code.
proofGPT models
Language models fine-tuned on the proof-pile.
1.3B model. 6.7B model.
proof-pile
8 billion tokens of mathematical text.
Dataset.
Mathlib Semantic Search
A semantic search engine for Lean mathlib based on the OpenAI API and Faiss.
with Ed Ayers
Demo. Code.
Lean Chat
An in-IDE chatbot that helps users formalize theorems in Lean.
with Ed Ayers
VS Code marketplace. Blog post. Client code. Server code. Hacker News.
particle_filtering
A mathematical exposition and NumPy implementation of particle filtering via SIS and the bootstrap filter.
Repo.