Keep the trusted part small.
The is the authority for proof acceptance. Everything that makes a proof easier to write or read belongs outside that logical trust boundary.
1. Inside the boundary
The checker, the syntax it depends on, structural proposition equality, and its context handling must be correct.
Soundness also relies on the chosen formal rules and on the runtime executing the implementation correctly. TypeScript types alone do not prove a theorem.
2. Outside the boundary
Editors, builders, tactics, search, parsers, pretty printers, and these lessons are .
A bug here may mislead a user or produce a bad candidate. It must never allow an invalid to bypass the checker.
3. The proof pipeline
The playground runs this construction-and-checking flow. Editing and automation are future extensions.
- Untrusted
Editor, builders, and automation
Construct a candidate. They cannot declare it valid.
- Evidence
Explicit proof AST
Carry every proposed inference step across the boundary.
- Trusted
Small kernel
Check the rules, assumptions, and resulting proposition.
- Result
Acceptance or rejection
Report the kernel’s verdict; never manufacture one in the UI.
4. Take this with you
Replace a builder, search algorithm, or UI freely; every candidate still passes through the same kernel. The playground executes this check for each selected example.