Welcome

Papers

Talks

Software

Essays

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.