Summary
Develop concrete plans for what to formalize in Lean and/or Agda, in what order, and with what tooling. The repository already has Lean 4 installed (via elan) and lean-lsp-mcp configured; this plan determines what mathematical content to formalize first and establishes the workflow.
Motivation
The repository contains mathematical specifications (semiotic universe, interactive semioverse, agential semioverse) that make formal claims. Formalization in a proof assistant turns those claims into verified statements. Without a strategy, formalization efforts will be scattered and disconnected from the specifications they should verify.
Steps
- Audit
content/mathematics/for formalizable claims — identify which objects, theorems, and structures are concrete enough to state in a proof assistant. - Evaluate Lean 4 vs Agda for the project’s needs (constructive reasoning preference per policy 004, category-theoretic content, available libraries).
- Choose a starting point: the simplest formalizable claim that exercises the toolchain end-to-end.
- Formalize the starting point and document the workflow.
- Write a prioritized list of subsequent formalization targets.
Done when
- Audit of formalizable content complete
- Lean vs Agda decision recorded
- First formalization committed and verified
- Prioritized formalization roadmap exists
Dependencies
None.
Log
2026-03-07 — Created from TODO.md unplanned item. Lean 4 toolchain already installed per plan 0015. lean-lsp-mcp configured.