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

  Eight 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 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