Specification
The design of Math 2.0. Start with the overview, then read the documents in order. Each document is also available as Markdown.
- Math 2.0: specification
- 01. The state of the field, October 2026
- 02. The goal
- 03. Architecture
- 04. The object model
- 05. The knowledge graph
- 06. Versioned storage: metadata, artefacts, provenance
- 07. The formal engine: Lean 4, Mathlib, proof checking
- 08. The computational engine: CAS, SMT, numerical experiments
- 09. Literature ingestion: papers, books, existing libraries
- 10. Autoformalization and statement fidelity
- 11. The Mathematical API and the agent orchestrator
- 12. Research agents
- 13. The research workspace: search, explore, explain, collaborate
- 14. Search
- 15. Trust and the audit
- 16. Collaboration and governance
- 17. Evaluation
- 18. Coverage: what "all mathematics" means
- 19. Milestones
- 20. Repository layout
- 21. Open questions
Math 2.0: the corpus specification
- Math 2.0: the corpus specification
- K01. Research
- K01, part A. Encyclopedic, reference and database sources of mathematics written by people
- K01, part B. Literature indexes, open textbooks and syllabi: sizes, licences, channels (research for math2)
- K01, part C. Formal libraries and formal / informal-formal datasets
- K01, part D. LLM generation at scale: quality, prior projects, memorization, law, terms and cost
- K01, part E. Representation, pedagogy, exercises, packaging and notation
- K02. The goal of the corpus
- K03. Identifiers: tags of ten characters
- K04. The inventory
- K05. Human sources
- K06. Formal sources
- K07. Machine generation: what models write, and how
- K08. The node card: what a good node contains
- K09. Quality: how the corpus stays correct
- K10. Structure, notation and conventions
- K11. Packaging: from nodes to courses, books and articles
- K12. Pipeline and operations
- K13. Law and ethics
- K14. Roadmap
- K15. Open questions