01 · the failure modesWhat carried it through wasn't cleverness
The agent ran for several sessions, hit real walls, and was stopped twice by its own tooling. What carried it through was a discipline: verify, checkpoint, hand off, and never trust a green build you didn't force. Three failure modes, recorded because they're the transferable part.
"Build completed successfully" — and it hadn't built the file
A full lake build reported green while the file being edited had twenty live
errors. The sharper truth (an external reviewer made us reconcile it) is that the library
root didn't yet import the module, so the default target never compiled it. The green was
target coverage, not verification. The rule: a green build is only real
if the module you touched actually recompiled and is in the build graph.
The decision that couldn't be a value (three times)
Proving decidability, the agent tried to build the decision as a value three
ways in a row — Lean won't case-split a logical disjunction to produce a computational
value. The fix was to prove it as a proposition, then lift via
Classical.choice. That's why the result is decidability-as-a-theorem, not a
runnable checker. The trap costs an agent hours and a human minutes, so it's written down
for both.
Stopped by its own tools, twice
A tool-call bookkeeping bug meant edits executed but results never came back — the agent could act but not see. The right move was to stop proving immediately (never write a proof blind) and hand off state to the next session. The project survived two dead sessions because handoffs, not memory, carried it.
02 · the honesty logErrors caught and recorded
(1) The stale-cache false W. (2) A replace_all corrupted 12 proof call-sites
on an overlapping pattern; fixed by reverting to a checkpoint, not patching the tangle.
(3) The canonical countermodel valuation was misread as needing to read from the
succedent; ground-truthing against the four-valued semantics confirmed the antecedent-only
reading was right all along — a tactic bug, not a design bug. (4) Three decision-value
architectures abandoned before the Prop-disjunction one landed. (5) External review
(2026-08-11) caught two overstatements: the false-W framing, and "constructive decision
procedure" for a result that is decidability-as-a-theorem. (6) A second artifact-audit
caught the Classical.choice attribution (factually wrong — inherited from
completeness, not the lift), an over-flat novelty claim, and a leaky
sorry-grep. All corrected; the reviewer confirmed the math holds. The full ordered log is
on the agents page.
03 · the build timelineGreens are rare and earned
Every reported lake build result across the five days. Upward ticks are green;
downward are red. The ringed tick is the one that matters most: a build that reported green
from stale cache while the source was broken — caught before the result was claimed.
04 · who caught itDiscipline, and openness, in one visual
Every failure, pitfall, and review catch, colored by who caught it. Most errors were caught by the agent's own verification discipline (dark); the external-review catches (violet) are the openness claim working in public. This is Kimi K3's proof; Rey and the second reviewer are peer reviewers, strengthening the artifact — not co-authors.
05 · activityNot one lucky run
Message volume per day — the dense completeness-repair day, the tool-outage trough, the publication-and-review tail. Texture, not headline; the build and failure lanes are the substance.
06 · what it costThe number everyone asks
The token spend for the proof, from real session telemetry (OpenRouter, Kimi K3) — the marginal cost of a formally verified result on an open-weight model, within reach of an individual researcher, not a lab.
| phase | sessions | input | output | cache-read | est. cost |
|---|
It's estimated, and internally consistent. The provider didn't return per-session actuals, so this is a modeled estimate, not an invoice. What's verified: the per-phase figures sum exactly to the totals, and the token volumes are real telemetry. The rate assumptions baked into the model (input ≈ $3/M, output ≈ $15/M, cache-read ≈ $0.30/M) sit slightly above OpenRouter's current Kimi K3 list price ($2.80/M in, $14/M out), so treat $63.34 as a defensible upper-bound estimate, not a precise figure. The honest read is "≈ $60, order-of-magnitude certain, internally consistent."
Cache is the real story. ~100M cache-read tokens (steep discount) against ~9.4M fresh input — without prompt caching this would have cost several times more.
The inefficiency is fixable. Half the total cost is one Aug 10 session where the 1M-token context re-ingests whole files. A more established setup — the lean4 skill that now exists didn't on Aug 7 — cuts it substantially.
07 · reproduceEvery claim here is checkable
The proof is a buildable Lean 4 project, and it is public: github.com/NimbleCoOrg/fde-lean. The verification recipe is the one actually run against it: module-targeted, not bare. It either reproduces the green build or it doesn't. Clone it and check.
Verification recipe (runs against the public repo)
git clone https://github.com/NimbleCoOrg/fde-lean && cd fde-lean export PATH=<elan>/bin:$PATH lake exe cache get # pull the precompiled mathlib cache — do NOT build mathlib lake build FDE.Corollaries # module-targeted — do NOT trust bare `lake build` grep -nE ":= *(by *)?sorry|admit|sorryAx|native_decide" FDE/*.lean # → empty # #print axioms decidable_deriv → [propext, Classical.choice, Quot.sound]
Toolchain: leanprover/lean4:nightly-2026-07-14. mathlib pinned f566658afd. Platform: aarch64-linux.
Artifact inventory (the repo map)
FDE/Basic.lean: four truth values, truth tables (ground-truthed by exhaustive evaluation), evaluation, designated-value set.
FDE/Sequent.lean: two-sided sequents, the invertible calculus, atomic + negated-atomic identity.
FDE/Soundness.lean: soundness by induction on the derivation.
FDE/Completeness.lean: inversion lemmas, the canonical countermodel, the weighted measure, completeness by strong induction.
FDE/Corollaries.lean: no-theorems, the disjunction property, and decidability of derivability (a theorem, not an executable checker).
The agent-facing account — environment constraints, the exact measure argument, the ordered failure log, the recreation recipe — lives on the agents page.
Every anchor in the figures carries the Discord message it was sourced from; the dataset
is generated by scripts/build-traces-data.mjs in the repo. The scrubbed
reasoning-traces archive — the full derivation record — lives alongside this page in
traces/.
The Lean proof itself is a separate repository (NimbleCoOrg/fde-lean),
a live Lake project, not a docs artifact.