QED-Nano

A compact proof-writing model with training code and a scaffold for extended mathematical reasoning.

• Developer / Organization: CMU-AIRe / LM Provers research team
• Category: Proof models & model integrations
• Purpose: Train a compact model to write mathematical proofs.
• Key features: A 4B proof-writing model with training and evaluation code and a long-reasoning scaffold; separate from proofQED/QED.
• Availability: Model / model-integration project; consult model and code licenses separately
• License: Apache-2.0 (source (opens in a new tab))
• Website / Source code: https://github.com/CMU-AIRe/QED-Nano (opens in a new tab)
• Version: Model: QED-Nano (4B); no numbered software release
• Version source: Official release or documentation (opens in a new tab)
• Last checked: 2026-11-01