Judge, don't build · Think Week

The situation#

Suppose you don't need to build much any more, because AI builds, but you do need to judge. The example here is ambitious on purpose: AI builds a formal math library, layer by layer (foundations → group theory → … → cohomology), and a proof checker verifies every step. What's left for the human?

Two questions:

Should you interfere in the build process at all, and where?
There's a finite set of things you must do. What is it?

Where to interfere#

A proof checker verifies that a proof proves its statement. It can't tell you whether the statement means what you meant. The same is true of tests and code: green tests prove the code does what the tests say, not that the tests say the right thing.

So interfere where the machine can't check the work and a lot depends on it:

	Little depends on it	Much depends on it
Machine can check it	UI, UX, helper functions, proof bodies → don't interfere	DSLs, tactics, tooling → test behavior hard, don't read the code
Machine can't check it	How readable a proof is → spot-check	Foundations, definitions, statements, the hierarchy → your job

A trap

Anything that definitions and statements are written in (like a DSL) isn't throwaway. It becomes part of what you have to trust.

The finite list, by weight#

#	Action	Weight	Why
1	Decide what the output is for, and who uses it. Include "why not extend the existing library (Mathlib)?"	10	The root. It sets the foundation, the style, and whether proofs must be readable.
2	Choose the foundation and the checker. Use an existing checker; never let AI build it.	10	Everything sits on it, and it's nearly irreversible. The checker is the only code you must fully trust.
3	Write or approve every definition and main theorem statement.	9	The checker can't catch a wrong definition, and a wrong definition makes every proof on top of it worthless.
4	Learn the subject one layer ahead of the build.	9	Without it you can't do #3 or #5.
5	Design the hierarchy: how general each concept is, what builds on what.	8	Decides whether the target is easy or painful 200 files later.
6	Write the blueprint: a target theorem plus the graph of definitions and lemmas leading to it.	8	Turns "a finite set of things" into an actual list. AI fills in the nodes.
7	Turn your rules into automatic checks: no unfinished proofs, approved axioms only, linters, naming, build-time limits.	7	Done once, then your standards run on every change without you.
8	Treat the AI's struggle as a signal, and schedule refactor reviews.	6	A way to judge the whole library without reading every proof.
9	Spot-check the structure of final proofs.	3	Only if people will read them. Otherwise the checker has done the job.
10	Throwaway parts: check they behave correctly, nothing more.	2	Nothing depends on how they're written.

How to judge a definition fast#

Tests for definitions, which work without reading any proofs:

Example: prove something that should qualify does (ℤ/2 is a group).
Non-example: prove something that shouldn't qualify doesn't.
Not vacuous: if nothing can satisfy a definition, AI will "prove" every theorem about it instantly. Proving one example exists catches this.
Two definitions agree: write a second, independent definition and prove them equivalent. Strong evidence both are right.
Edge cases: the empty set, n = 0, the trivial group, division by zero.

Signals that something upstream is wrong#

A long proof of an "obvious" fact → a bad definition or missing basic lemmas.
Many near-duplicate lemmas → a missing abstraction.
Automation keeps failing in one area → the hierarchy is wrong there.

Making "learn it" finite#

Learn only the nodes in the blueprint, just before the AI builds them. The rule: you can explain every definition in the blueprint without looking anything up. Don't study a topic until it's the next node. AI tutoring makes this fast.

Why this chapter is about more than math#

Swap "formal math library" for "product", "codebase" or "business" and the table still holds. The machine-checkable, low-stakes parts (UI details, helper code, first drafts) are where AI should run free. The unverifiable, high-stakes parts are what the business is for, who it serves, the core definitions (what's the product, what's the promise) and the structure everything sits on. Those are the human's job, and they're the "taste and judgment" from Chapter 5, made concrete.

Where to spend your judgment

Interfere where the machine can't check the work and much depends on it. Automate your standards everywhere else.

Takeaways

A checker proves consistency, not meaning. Meaning is your job.
Own the root decisions: purpose, foundation, definitions, hierarchy.
Encode your standards as automatic checks, then stop reading the rest.
Pick the target first ("the long exact sequence in group cohomology"), then work backwards. "Start small" names an area, not a target.