القائمة
Transferable lessons from the first complete FormalFrontier book formalization (Sutherland Number Theory Lecture 1). Use when planning or executing future book formalizations.
التثبيت باستخدام Codex أو Claude انسخ هذا Prompt والصقه في Codex أو Claude أو مساعد آخر ليراجع صفحة Skill ويثبّتها لك.
استنادا إلى تصنيف SOC المهني
| name | project-retrospective |
| description | Transferable lessons from the first complete FormalFrontier book formalization (Sutherland Number Theory Lecture 1). Use when planning or executing future book formalizations. |
| allowed-tools | Read, Bash, Glob, Grep |
First complete FormalFrontier formalization. 27/27 formalizable items sorry-free in ~5.3 hours of parallel agent execution on 2026-03-16. 46 merged PRs, 59 issues created.
Stage 2.4 (Mathlib Coverage) and Stage 2.7 (Reference Attachment) together took ~1 hour but saved ~3 hours during proof filling:
inferInstance — no creativity needed..refs.md files (PR #63) pre-curated exact Mathlib declaration names per item. Agents could copy-paste API names instead of searching.Transferable rule: Always complete Stages 2.4 and 2.7 before any scaffolding. The coverage percentages predict formalization velocity: >70% Mathlib coverage = fast project; <50% = expect significant proof work.
Stage 3.1 scaffolded ALL 27 items with sorry placeholders across 5 batches (PRs #67, #69, #73, #93) before ANY proof was filled. Benefits:
items.json status tracking worked cleanly from day oneTransferable rule: Complete all scaffolding (Stage 3.1) before starting any proof filling (Stage 3.2). Never interleave.
Every PR targeted a specific deliverable (1-3 related items). Auto-merge via gh pr merge --auto --squash meant agents never waited for human review. Average cycle: PR created → merged in 10-15 minutes (CI time).
Transferable rule: Keep PRs small (1-3 items). Enable auto-merge immediately. Don't batch unrelated items.
Two primary agents (1d7941eb, 15903d7e) worked simultaneously on different proof items without merge conflicts. The key enabler: items in separate Lean files with no shared state.
Transferable rule: One Lean file per item during scaffolding. This enables embarrassingly parallel proof filling.
After completing ~50% of proofs, agents documented 8 proof patterns in lean-proof-strategies skill (PR #94). The remaining 50% of proofs went faster because agents could match new items to known patterns.
Transferable rule: After 40-60% of proofs are done, pause to document proof patterns. The skill pays for itself on the remaining items.
Theorem 1.9 (Product Formula) — 113 lines. Required decomposing a product over all primes into numerator/denominator factors using coprimality of reduced rational form. Heavy padicNorm and FTA API usage.
Example 1.24 (Z[sqrt(5)] not integrally closed) — 139 lines. Required Algebra.adjoin_induction, irrationality of sqrt(5), and a contradiction via fraction ring lifting. Most complex proof in the project.
Example 1.29 (Non-integral element) — 64 lines. Required showing minimal polynomial has non-integer coefficients via conjugate integrality and algebraic computation.
Key lesson: Counterexample proofs (Examples 1.24, 1.29) were harder than forward proofs. They require constructing specific algebraic objects and deriving contradictions — no standard Mathlib API for this.
Several proofs hit "motive is not type correct" errors when using rw on terms appearing in dependent types. The solution (documented in lean-proof-strategies) is to generalize first with suffices, then instantiate with convert.
Transferable rule: When planning proof difficulty, add +1 difficulty level for any proof involving rewriting inside dependent types (common with integral closures, subtype coercions, and scalar towers).
items.json drifted from reality during rapid parallel work (PRs #83, #88 were just status corrections). Two agents updating the same JSON file led to stale reads.
Transferable rule: Status corrections should be a dedicated review task after each batch, not expected to stay accurate during parallel work.
| Strategy | Predicted (Stage 2.6) | Actual | Items |
|---|---|---|---|
| inferInstance | 5 | 6 | Props 1.22, 1.25; Cors 1.21, 1.23; Defs 1.12, 1.13 |
| Direct Mathlib API (1-line) | 9 | 8 | Thms 1.8, 1.16; Props 1.18, 1.20, 1.28; Def 1.7; Cor 1.5.2; Def 1.26 |
| Instance transfer | 2 | 2 | Prop 1.25 (alt), Def 1.17 |
| Short tactic proof (2-10 lines) | 5 | 5 | Ex 1.14, 1.15; Cor 1.5; Def 1.6; Def 1.10 |
| Case-split construction | 1 | 1 | Ex 1.3 |
| Algebraic identity + order | 1 | 1 | Cor 1.5.1 |
| Calc chain / helper lemma | 2 | 2 | Lemma 1.4, Thm 1.9 |
| Contradiction / counterexample | 2 | 2 | Ex 1.24, Ex 1.29 |
Accuracy of Stage 2.6 predictions: 96% (1 item shifted from "API call" to "short tactic"). The readiness report is reliable.
This project completed 27/27 items without Aristotle. In retrospect:
Heuristic for future books: Escalate after 2 genuinely different approaches fail AND the proof requires >80 lines of Lean. Short proofs that fail are usually a sign of wrong statement formalization, not proof difficulty.
For number theory lectures at this level (introductory algebraic number theory):
abbrev or type alias)Use when deciding whether a formalized proof should delegate to Mathlib, when refactoring standalone proofs into Mathlib wrappers, or when reviewing delegation refactors for correctness.
Use when running Stage 3.4 (Proof Polishing) to bring sorry-free proofs to Mathlib quality. Use when assessing whether a proof needs cleanup, when working through proof-polish GitHub issues, or when deciding which tactic to prefer for a given goal.
Use when a Lean proof has failed 2-3 attempts and needs to be sent to Aristotle for automated proving, or when checking the status of a previously submitted Aristotle job.
Quantitative insights on formalization speed by item type and proof strategy. Use when estimating difficulty from textbook statements, planning batches, or predicting project timelines.
Use when filling sorry placeholders in Lean 4 proof files, when choosing between proof approaches for a FormalFrontier item, or when a proof attempt fails and you need an alternative strategy.
Use when searching for Mathlib declarations to fill a proof, when imports fail, when you need to find the right Mathlib module for a concept, or when exact? or apply? don't find what you need.