| name | formalization-velocity |
| description | Quantitative insights on formalization speed by item type and proof strategy. Use when estimating difficulty from textbook statements, planning batches, or predicting project timelines. |
| allowed-tools | Read, Bash, Glob, Grep |
Formalization Velocity Model
Data from the first complete FormalFrontier formalization: Sutherland Number Theory Lecture 1 (27 items, 46 PRs, ~5.3 hours total with 2 parallel agents).
Item Type Velocity
Measured from Sutherland Lecture 1. Times include scaffolding + proof filling per item.
| Item Type | Count | Avg Lines | Avg Time | Mathlib Wrapper % | Notes |
|---|
| Definition | 9 | 25 | 5 min | 100% | Always Mathlib wrappers or abbrev |
| Proposition | 5 | 28 | 10 min | 80% | Usually inferInstance or 1-line API |
| Corollary | 3 | 30 | 8 min | 100% | Always follow from parent theorem |
| Theorem | 3 | 63 | 30 min | 67% | Named theorems often in Mathlib; product formula was outlier |
| Lemma | 1 | 85 | 45 min | 0% | Required original calc chain proof |
| Example | 4 | 69 | 35 min | 25% | Counterexamples never in Mathlib |
Key insight: Definitions and corollaries are always fast. Lemmas and examples (especially counterexamples) are the slowest.
Proof Strategy Speed Ranking
| Strategy | Items | Avg Lines | Avg Time | When to Expect |
|---|
inferInstance | 6 | 23 | 3 min | Typeclass properties (IC, UFD, field) |
| Direct API call | 8 | 28 | 5 min | Named theorems, standard results |
| Instance transfer | 2 | 30 | 8 min | Properties via equivalence/isomorphism |
| Short tactic (2-10 lines) | 5 | 35 | 15 min | Setup + exact, localization results |
| Case-split construction | 1 | 39 | 20 min | Building new structures field-by-field |
| Algebraic identity + order | 1 | 63 | 25 min | Char p results, finite field proofs |
| Calc chain / helper | 2 | 99 | 45 min | Inequality chains, density arguments |
| Contradiction / counterexample | 2 | 102 | 60 min | "Not X" proofs, specific ring examples |
Difficulty Prediction from Textbook Statement
Fast Signals (expect <10 min)
- Statement says "X is a Y" where both X and Y are standard Mathlib types
- Statement says "follows from" or "by [named theorem]"
- Statement is a corollary of the previous item
- Definition matches a Mathlib typeclass exactly
Medium Signals (expect 15-30 min)
- Statement requires a short proof using a specific Mathlib lemma with setup
- Statement involves localization, completion, or quotient constructions
- The .refs.md file lists a Mathlib declaration but with caveats
- Statement involves instance transfer across an equivalence
Hard Signals (expect 45-90 min)
- Counterexample proofs ("X is NOT Y"): Always hard — requires constructing specific objects
- Product/sum formulas: Require decomposition + recombination over finite sets
- Characterization lemmas ("X iff for all n, P(n)"): Often need density/limit arguments
- Algebraic identities in non-commutative or graded settings: Cast mismatches, dependent types
- The .refs.md file says "no direct Mathlib coverage" or "partial coverage"
Red Flags (consider Aristotle escalation)
- Statement involves a product over all primes (infinite product reasoning)
- Statement requires irrationality proofs of algebraic numbers
- Proof sketch in the textbook uses "by a standard argument" without details
- Multiple ring extensions with scalar tower interactions
Mathlib Coverage Heuristics
For introductory algebraic number theory (undergraduate/early graduate level):
| Content Type | Expected Mathlib Coverage |
|---|
| Standard definitions (DVR, PID, UFD, integral closure) | 95%+ |
| Named theorems (Ostrowski, Dedekind, Minkowski) | 80%+ |
| "Follows from" propositions | 70%+ |
| Worked examples (specific rings like Z_p, k[[t]]) | 50% |
| Counterexamples (Z[sqrt(5)] not IC) | 0% |
| Product/summation formulas | 30% |
Rule of thumb: coverage% * 0.7 + 30 = expected % of items provable in <10 min
For this project: 74% * 0.7 + 30 = 82%. Actual: 22/27 = 81%.
Batch Sizing Guidelines
Based on observed throughput with auto-merge PRs:
| Batch Type | Items per PR | Agent Time | Rationale |
|---|
| Scaffolding (Stage 3.1) | 5-8 | 30 min | Parallel-safe; no proof work |
| Easy proofs (inferInstance, API) | 3-5 | 20 min | All trivial; group by topic |
| Medium proofs | 2-3 | 30 min | Related items share imports |
| Hard proofs | 1 | 45-90 min | Need full agent attention |
Total throughput: 2 agents can do ~12-15 items/hour on easy, ~4-6/hour on medium, ~1-2/hour on hard.
Project Duration Estimation
Given a textbook section with N formalizable items and C% Mathlib coverage:
Phase 1 (source prep): 1 + 0.15 * pages hours
Phase 2 (dep mapping): 1 + 0.05 * N hours
Phase 3 (formalization):
Easy items: N * C% * 0.15 hours
Medium items: N * (1-C%) * 0.6 * 0.4 hours
Hard items: N * (1-C%) * 0.4 * 1.2 hours
Total with 2 agents: (Phase 1 + Phase 2 + Phase 3) / 1.6
For Sutherland Lecture 1 (9 pages, 27 items, 74% coverage):
- Phase 1: 1 + 0.15*9 = 2.35h
- Phase 2: 1 + 0.05*27 = 2.35h
- Phase 3: 270.740.15 + 270.260.60.4 + 270.260.41.2 = 3.0 + 1.7 + 3.4 = 8.1h raw
- With 2 agents: (2.35 + 2.35 + 8.1) / 1.6 = 8.0h
Actual: ~5.3h (faster due to high parallelism in Phase 3 and aggressive batching).
Lines of Lean Per Item Type
Useful for estimating file sizes and review effort:
| Difficulty | Lean Lines (with imports) | Proof Lines Only |
|---|
| Trivial (inferInstance) | 20-25 | 1 |
| Easy (API call) | 25-35 | 1-5 |
| Medium (short tactic) | 30-50 | 5-15 |
| Hard (calc chain) | 60-100 | 30-70 |
| Very Hard (counterexample) | 80-140 | 40-100 |
Total project: ~1,200 lines of Lean across 27 files.
