Studying
Studying
Operational-axis Lean4 kernel + cross-axis representation research. Axiomatizes qagents operations (git first) with the same kernel + LLM-facts + lake-build architecture as proving/ and accounting/; owns the hub/ guide-rails. T1 (branch-lock exclusion) and T3 (worktree divergence detection) proved by the /dao coding-v.-testing lane over extracted repo snapshots.
version leanprover/lean4:v4.30.0
source studying/lean-toolchain
built 2026-06-13T17:08:37.311Z
OK Diagrams pending (operational kernel)
Workflow views mount in monitoring/ (local-only) via the kit-mount pattern; the /status card carries metrics only.
Metrics
- focusAreaCount
- 10
- toolchain
- leanprover/lean4:v4.30.0
- theoremsProved
- 3
- daoRounds
- 2