Issue 02: Attention is Not All You Need

Transformers are great, but LLMs have an attention problem. They are easy to distract when deciding what deserves attention over the course of a long, uncertain research trek. That is the hard-earned lesson of this SATurday installment; machine models have rudimentary mathematical knowledge and can produce useful deductions, proof sketches, counterexamples, and even formal code. Provide an agent a frontier problem and enough time, however, and it can happily spend it generating certificates of nothing. SATurday’s solution is not to use smarter models and hope they make better choices; rather, it is to make the problem smaller. Before we talk architecture, below is the research context.

A Prelim

SATurday is a research project toward P vs NP whose bet is emphatically not “ask a chatbot for a proof.” The route this project explores is proof complexity, the study of how large a proof must be inside a particular formal proof system (lecture notes). We know explicit families of formulas for which weak systems require enormous computational proofs. Stronger systems are even harder to understand. At the far end, Cook-Reckhow connects sufficiently strong propositional proof systems to the complexity classes NP and coNP. This territory is already established mathematics, which runs directly into major open problems in proof complexity.

SATurday’s research ladder is a map across proof complexity territory, formalized in code. The idea is to break apart uncharted territory into small, falsifiable pieces, called rungs. A rung is one claim on the chain: a foundational axiom, a lower bound, or a bridge theorem. Each rung has a mathematical statement, a status, a Lean home, and a memory file to which it is written. Finally, a rung is stateful and can be classified as open or closed. Closing a rung changes what the system is allowed to treat as ground truth. Until Lean accepts the relevant declaration with zero sorry, or no ambiguity, it does not count as formally certified.

The distinction between assumed and certified matters. Lean can verify that a formal theorem follows from its stated assumptions, but cannot magically guarantee that what was formalized was what was intended. Humans still have to inspect the correspondence between the mathematics on paper and those in code. Hence, the rungs serve two purposes, to organize the mathematics and constrain the agent’s attention.

The agent works on one claim. It records what happened. Then it stops. If it succeeds, the next wake cycle inherits a stronger foundation. Fail, and a claim is discarded. The agents thrash and trash, generating logs of hallucinations which look like progress.

We implement a smart system to reduce hallucinations. A smart system, however, does not mean a bigger model. It means a deliberately boring mechanical loop wrapped around a relatively small local model, broken up into the following four stages:

Pick one rung → run one stage → check the result → write to memory → stop.

Humans still gate progression across the research tree. The intelligence here rests increasingly in the harness rather than the model size or parameters.

SATurday climbs toward P vs NP through a locked proof-complexity ladder made of falsifiable claims. The premise is simple: don’t ask a machine to solve one enormous problem. Decompose it into smaller claims whose truth or falsity can be tested.

Each accepted rung is formalized in Lean 4 with zero sorry on the accepted declaration. In practical terms, Lean forces every accepted claim to rest on previously checked definitions, theorems, and allowed axioms. Though this is enormously useful, it is also a trap. Spelling mathematics out so that a machine can check every logical dependency is a slow, meticulous, and fractal-like process. A two-line argument on paper can explode into definitions, helper lemmas, coercions, edge cases, imported methods, proof obligations, and even vagueness. A model with finite context eventually drowns in residue. This issue can be attacked with larger models, bigger context windows, enormous memory, and ungodly parallelism. Alternatively, you can try making the thing the model is allowed to think about much smaller. SATurday does the latter.

Smart Systems to Address LLM Lack of Focus

SATurday currently runs much of its inference locally, including small Qwen-class models on a personal MacBook. That constraint is intentional. The premise is to “dumb down” math theorems with smart systems that require less unconstrained “thinking.” SATurday is less interested in whether a giant frontier model can produce a brilliant mathematical continuation than whether a small model becomes substantially more useful when the surrounding software narrows its job.

SATurday’s loop is deliberately mechanical. Each wake loads the P vs. NP proof ladder state, picks one rung/claim, and applies a deduction stage. Available stages are prove, audit, formalize, or falsify.

Stages

·Prove constructs a mathematical argument in prose.
·Audit attempts to break the argument by any means necessary. Here, an LLM inspects the proof against predefined failure criteria: vague constants, hidden assumptions, unjustified asymptotics, circular dependencies, quantifier mistakes, or a lemma that quietly assumes the thing it is trying to prove.
·Falsify avoids LLM calls where possible, and runs ordinary computational tools and solvers against finite instances of the claim. It looks for counterexamples and checks whether the proposed bounds behave the way the argument says they should.
·Formalize translates the surviving argument into Lean 4, where the kernel gets the final word on whether the formal statement actually makes sense.

It writes to memory, logs one session line, and stops. Ideally, there is no wandering off to a more interesting theorem, deciding midway through that P vs NP would be easier through an unrelated route, or a twenty-page monologue to use up tokens. Consider our current R2 rung falsify wake: the active claim states that a particular family of Tseitin formulas must have large resolution width. The agent receives the following prompt:

Here is the exact width claim and its dependencies. Here is what previous wakes established. Your job is to try to falsify it.

The agent searches for a counterexample, tests permitted instances, records the result, updates the rung’s memory, and exits. A later wake might audit the surviving argument, and another following wake might formalize one lemma. The final wake might discover that the whole direction is garbage. All outcomes are useful because the unit of work is small enough that failure is decisive and digestible. This is engineered attention.

Assuming our proofs can survive these gauntlets, we produce a Lean certificate, which can then be interpreted by a human and sent off to publication!

This is, of course, an idealistic loop. There is an obvious problem with all of this. A research agent that cannot reliably distinguish an important lemma from an attractive dead end will certify noise forever. Formal verification does not solve that problem.

Lean is extremely good for answering a particular class of questions. Does this theorem follow from these definitions and assumptions? Yes, or perhaps no. However, our loop cannot answer fundamental mathematical pondering. Is this theorem useful? Was what was formalized what was actually on paper? Is spending the next six months proving this lemma a good idea? Without dedicated systems and guardrails, our agents are just as lost as we are when attempting to solve frontier problems.

So SATurday adds another constraint to try to speed up the process: organized parallelism. Certain rungs or claims are unrelated and do not collide (for example, R2 vs R5), and can be explored at will ad infinitum. Those workstreams can therefore run in parallel while still obeying their own rung boundaries. But parallelism introduces another failure mode: instead of one agent generating trash forever, you can have ten agents generating trash ten times faster. SATurday therefore includes plateau detection, a monitoring dashboard, and a manual kill switch. Attention is therefore enforced by our software architecture and human guidance.

A Note on Our Rungs

The full ladder lives in `docs/ladder/ladder.md`, with individual rung files under `docs/ladder/rungs/`.

Acceptance means Lean 4 with zero sorry on accepted declarations, under the project’s allowed axioms.

Rung	Status	Idea	Formal	Summary
R0 · Resolution Robinson, 1965	Certified	Resolution repeatedly combines clauses by eliminating a contradictory variable. If this process derives contradiction, the original Boolean formula cannot be satisfied.	A resolution calculus with $\mathsf{Derivation.size}$ , plus soundness and refutational completeness in `Resolution.lean`.	Cancel one variable at a time; you can derive contradiction exactly when the CNF has no satisfying assignment.
R1 · Haken PHP Haken, 1985; bottleneck formulation following Beame-Pitassi, 1996	Certified	The pigeonhole principle gives an explicit family of formulas that resolution cannot refute efficiently. Detail Haken’s lower bound shows that such proofs eventually pass through clauses of intermediate complexity. Only a limited number of assignments can survive each of those clauses, so the proof must contain exponentially many of them.	$\forall n \ge 288$ , every resolution refutation $d$ of $\mathtt{phpCNF}\,n$ satisfies $2^{(n-3n/4-36)/35} \le d.\mathsf{size}$ implemented as `php_resolution_size_lower_bound`.	Every proof must pass through a narrow bottleneck, and too few assignments fit through each opening, so exponentially many clauses are required.
R2 · Width / families Ben-Sasson-Wigderson, 2001; Chvatal-Szemeredi, 1988; Urquhart, 1987	Prose accepted; item 2 open	Build reusable width-to-size lower-bound machinery, then apply it to hard formula families beyond a single example. Detail Ben-Sasson and Wigderson relate clause width in a resolution proof to proof size: if every refutation must contain very wide clauses, then every refutation must also be very large. Candidate families include random $k$ -CNF and Tseitin formulas on expander graphs. Remaining work: width lower bounds for those families.	$\mathrm{width} \ge W \Rightarrow \mathrm{size} \ge 2^{(W-\mathsf{cnfWidth})^2/(c\cdot\|V\|)}$ implemented as `bsw_size_lower_bound`.	If large width is forced, large size follows; random $k$ -CNF and expander Tseitin are the candidate families.
R3 · Above resolution Pudlak, 1997; Ajtai, 1988; Pitassi-Beame-Impagliazzo, 1993	Proposed	A super-polynomial size lower bound for a proof system strictly stronger than resolution. Detail Candidate systems: $\mathrm{Res}(k)$ , cutting planes, or bounded-depth Frege.		Certify hardness one simulation level above resolution.
R4 · Open frontier Razborov, 1987; Smolensky, 1987	Proposed	A super-polynomial size lower bound for $\mathrm{AC}^0[p]$ -Frege, then $\mathrm{TC}^0$ -Frege, Frege, and Extended Frege. Detail Related $\mathrm{AC}^0[p]$ circuit lower bounds exist (Razborov, Smolensky). Matching Frege-style proof lower bounds do not.		$\mathrm{AC}^0[p]$ circuit hardness is known; $\mathrm{AC}^0[p]$ -Frege hardness is the open target.
R5 · Cook-Reckhow Cook-Reckhow, 1979	Active	A polynomially bounded propositional proof system exists exactly when $\mathrm{NP} = \mathrm{coNP}$ . Detail R5 opens after the resolution foundation rather than after every lower-bound rung above it. SAT has short certificates for yes instances (satisfying assignments). A polynomially bounded propositional proof system would give the same for tautologies. SATurday formalizes $\mathsf{InP}$ , $\mathsf{InNP}$ , $\mathsf{IsPropProofSystem}$ , and $\mathsf{TM2ComputableInPolyTime}$ , with the implications linking polynomially bounded proof systems to NP/coNP and to P vs NP.		If every propositional proof system requires super-polynomial proofs somewhere, then $\mathrm{NP} \neq \mathrm{coNP}$ , and since $\mathrm{P} = \mathrm{NP}$ would imply $\mathrm{NP} = \mathrm{coNP}$ , that would give $\mathrm{P} \neq \mathrm{NP}$ .

Conclusion

How much mathematical research can a small model do when it is never asked to be a mathematician all at once? Attention is not something we should trust our models have. SATurday is trying to build a framework around it.