Grace17 documentation

Start with the introduction. It explains why Grace17 is built on set theory, walks through first proofs, and tours the larger developments in Cumulus.

Language#

• Definitions: def, predicate, class, recursion, and their proof obligations
• Ordinals: von Neumann ordinals and executable Cantor normal forms
• Datatypes: inductively defined classes of sets, and structure declarations for groups, rings, orders, and categories
• Types and instances: soft types, classes, and instance resolution
• Notation: mathematical notation, Unicode and ASCII, and notation declarations
• Proving theorems: writing statements and proofs, applying theorems, and using the automation
• Tactic reference: every tactic, organized as in the Workbench Help, with examples and rule schemas
• Modules, namespaces, and sections: how files, imports, names, and shared hypotheses organize a development

Cumulus, the mathematics library#

• Cumulus guide: what is proved, organized by subject
• Top 100 theorems: formal statements and proof links
• Erdős problem 397: an infinite family of binomial coincidences, found with an AI, checked from the axioms
• Algebraic hierarchy: how structures are represented
• Axiom audits: inspecting Choice and other assumptions a proof uses

Community#

• Community: Zulip chat, GitHub, how to cite, and how to contribute mathematics

Trust#

• Foundations: the foundation contract and the ZF, ZFC, and ZFG profiles
• Natural deduction certificates: every proof as a Fitch-style or Gentzen-style derivation you can read
• Soundness: what is trusted, independent checkers, and the path to proved checkers
• Checker semantics: the proof checker as a small-step transition system, the definition every independent checker implements
• Kernel format: the normative G17M proof-tape specification
• Compiled module format and foundation bootstrap: G17C
• Conformance: the executable compatibility corpus for checkers
• Ground evaluation: the trusted evaluator behind compute
• Independent checkers: the Python, OCaml, and Rust checkers

For AI agents#

• Grace17 for AI agents: the checking API, goal states, search, and a working loop for agents that prove theorems
• Machine interface: g17 serve and the method subcommands, the JSON protocol that exposes what the Workbench shows
• Claude Code users: /plugin install grace17 --marketplace grace17-prover/grace17 installs the Grace17 skill
• AGENTS.md: expectations for coding agents that modify Grace17 itself

Tooling#

• Architecture: how the system fits together, for people working on Grace17 itself
• Workbench: the browser proof assistant
• Library search
• External libraries: developing mathematics outside the Grace17 checkout
• Website: building the static site, Cumulus browser, and embedded Workbench