{"path":"research/alien-proofs-and-the-library.md","content":"# Alien proofs and the library: what a tidying problem in mathematics shows about ours\n\n**Date**: 2026-10-10 · **Type**: a public post read against the corpus and against six outside\nsources · **Status**: analysis. Every position below that is not quoted from a ruling is Claude's\nand unruled (ledger Arc AF).\n\n**Source**: a public post on Facebook (8 October 2026, several hundred words) about the pull between\na library of formal mathematics that people curate and proofs that a machine finds on its own. The\nlibrary is Mathlib, the main library of the Lean proof assistant. The author is not named on this\npage, because the page says where the post overstates. The name, the link and a fuller account are\nheld privately (`.private/sources/fb-post-alien-proofs-and-mathlib-2026-10-08.md`).\n\n**The founder's instruction**: *\"Mine this for insights!\"*\n\n**Who wrote this reading**: a language model. The post's author has not been told that the post\nwas read here. Whether to tell them is the founder's to decide.\n\n**Read depth**: the post, its image and its comments in full, in a browser, on 2026-10-10. Outside:\nMathlib's contribution guide and four paper abstracts were read directly; passages inside three of\nthe papers came through a reader that answers questions against the page, and are given here in\nother words. No paper was read in full (§ 7). The corpus notes named below were read this session\nin the sections cited.\n\n---\n\n## 0. In short\n\n1. **The post describes a real line of research and overstates how far it has come.** Machine-written\n   proofs do come out correct and hard to read, and since 2024 a second machine has been set to tidy\n   them. The library's own keepers wrote in mid-2026 that such code misses their standard \"by a\n   large margin\" when no expert supervises it, and their queue of waiting submissions grew from\n   about 1,500 to over 2,600 in about a year.\n2. **The checker stops at the proof.** Lean decides whether a proof is correct. Nothing decides\n   whether it belongs in the library, at what generality, under which name. About thirty people\n   settle that, and the newest paper on tidying argues that length, the one thing a program can\n   score, is the wrong score. The corpus said in September that reuse in mathematics is judged and\n   not decided. These are the numbers.\n3. **A result can be accepted before anyone understands it only where something other than a\n   reader checks it.** A proof checker can, and so can an experiment. For a weighing, a value, or\n   the step from one claim to another, nothing can. There, being followable is the check, where in\n   mathematics it is a later improvement.\n4. **Take correctness out of the post's reward and what is left pays for two of this project's\n   known errors.** \"Shorter\" pays for leaving things out. \"In the house style\" pays for forcing new\n   material into old shapes.\n5. **Two different things are called shortening.** Pointing at something a reader can open loses\n   nothing. Leaving steps out does. A word count cannot tell them apart.\n6. **A prover makes a wide rule safe, and without one the default should be narrow.** Mathlib asks\n   for the most general statement that can be proved, because one that is too wide fails to prove.\n   Here a wider rule only adds cases nobody checked. Proposed: a rule a machine writes under a link\n   is worded over a group of links, as narrowly as covers them. ⚠ *Revised the same day (§ 6b): this\n   holds for steps from a rule and a case only, the rule is a guess that the links prompt, and\n   narrow is where the guess starts.*\n7. **Three smaller things to take**: a test with a known answer for the pass that writes out\n   unwritten rules; a mark on machine work that says which mistakes to look for; and one more\n   reason why outside agents should read the graph and not write to it.\n\n---\n\n## 1. What the post says\n\nIn other words, and shorter than the post:\n\n- **Machine search can reach a proof that the compiler accepts and that goes around the library.**\n  It is specific, low-level and close to the axioms, and people cannot easily read it, teach it or\n  fit it in. The post calls this an alien proof. Its image is the many-eyed creature that\n  discussions of language models use for what lies behind a model's friendly surface.\n- **The library's rule is generality.** Everything is stated as widely as it can be. Definitions\n  made for one problem would pile up as debt and duplicates.\n- **Search from the ground up fails alone**, because the possible steps multiply. The library's\n  concepts shorten the search: one named concept stands for many small steps.\n- **The proposed way through has two stages.** A system finds a raw proof. A second system rewrites\n  it in the library's manner (pulls out lemmas that could be used again, names them properly,\n  restates the argument at the library's level) and only then offers it to the library.\n- **Five techniques are listed**: a prover paired with a tidier; finding pieces of proofs that\n  repeat and making them lemmas; training a tidier on clean proofs that a program has expanded into\n  small steps, so that it learns the way back; a reward with three terms (the proof compiles, it is\n  shorter, it passes the style checks); and a check that tidying has not changed what a lemma\n  states.\n\nThe post names no source. One commenter remarks that machines lose detail when they summarise or\nredo something.\n\n---\n\n## 2. What of it holds\n\n| The post | What the sources read here show |\n|---|---|\n| Machine proofs are correct and alien | In kind, yes. A 2024 paper says one well-known system's proofs had a strange structure unlike a person's (ImProver). Two 2026 papers describe machine-written Lean proofs as correct, long-winded and fragile when the library changes version (Lean Refactor), and as single blocks with reusable arguments left inline, definitions made for one problem, and heavy automation (Proof-Refactor). The published complaint is clumsiness. None of the three describes a shortcut near the axioms, and the proofs in question depend on the library: they break when its version changes. |\n| The library demands generality | Yes. Its guide names generality, fit with the rest of the library and ease of upkeep as the standard. |\n| The library's concepts make search tractable | The usual view. Not checked against a source this session. |\n| A second machine can tidy | Under study. Shortening works by the papers' own counts: over 70% fewer tokens on competition problems and over 20% on research code (Lean Refactor). Structure is harder. Proof-Refactor says the measures that can be computed are mostly about length, that readability and reuse resist a dependable automatic measure, and it scores its own result on a five-part rubric that a language model fills in. |\n| The tidied proof is then filed with the library | Not as of mid-2026. The guide says machine-written code with no Lean expert supervising misses the standard \"by a large margin\", that poor submissions of this kind are closed without comment, and that an author must be able to defend every decision without a machine's help. |\n| Tidying can change a statement | The check exists for the theorem itself: both versions are compiled as proofs of one statement (Lean Refactor). Whether a formal statement says what was meant is beyond any compiler, which the corpus holds from two earlier readings (§ 3). |\n\n**The numbers.** Mathlib had about 30 maintainers and about 1,500 submissions waiting when its\nmaintainers described the library in a paper of August 2025. Its guide says over 2,600 are waiting\nin mid-2026, and advises anyone in a hurry to build outside the library. An earlier note here\nrecorded a paid review effort started against a queue of over 2,000\n([lean-social-system-research.md](lean-social-system-research.md)). So the queue grew by about three\nquarters in about a year. These pages do not say how much of that growth is machine-written.\n\n**By this project's own rule the tidying results are findings.** A person reads what a machine pass\nproduced before anyone proves how often it is wrong (principle of 2026-10-06). Proof-Refactor's\nmain result is a score given by one model to another model's work.\n\n---\n\n## 3. What the corpus already held\n\nSo that what follows is not taken for new where it is not:\n\n- **Reuse in mathematics is judged.** A large formalisation that came out five times the size of the\n  library was read here as a graph with no merge pass, with the sentence that even where identity\n  is free, the reuse layer is judged and not decided\n  ([formalized-fermat-and-the-oracle-boundary.md](formalized-fermat-and-the-oracle-boundary.md)).\n- **Checked is not yet understood.** A machine-made proof is born needing an exposition\n  ([understanding-after-the-proof-machines.md](understanding-after-the-proof-machines.md)).\n- **Laws for code, samples for judgements, and a small trusted checker.** With one law measured as\n  broken: the graph does not come out the same when its sources arrive in another order\n  ([bend-and-deliberus.md](bend-and-deliberus.md) § 4, § 5; ledger T4).\n- **The library's own upkeep**: an old name is kept for some months and then removed, and the rules\n  it uses for rewriting must simplify, must not depend on order and must come to an end\n  ([lean-social-system-research.md](lean-social-system-research.md)).\n- **The flywheel of reuse needs identity to be cheap to decide**, and one earlier sentence, that\n  Mathlib names the design direction, is struck through there and stays struck\n  ([the-reuse-flywheel-prior.md](the-reuse-flywheel-prior.md)).\n\nWhat the post and the sources behind it add is below.\n\n---\n\n## 4. What it adds\n\n### 4.1 The checker stops at the proof\n\n**Mathematics has a perfect checker of truth and still runs its library on judgement.** The kernel\naccepts or refuses a proof. Whether the result is stated generally enough, sits in the right place,\ncarries the right name and duplicates nothing is decided by reviewers, and they are the bottleneck:\nabout thirty maintainers, and a queue that passed 2,600. Proof-Refactor describes the same gap from\nthe research side, as a mismatch between what is easy to check and what a library needs.\n\n**So the absence of a truth checker here is a real difference for the raw layer and none for the\nlibrary layer.** What a contributor or a machine first puts into the graph is unverified, where a\nraw proof is verified (§ 5). The work of making it usable (same or different, general enough,\nfiled where) has no checker in either field. That work is most of what Deliberus does, and it is\nthe part of mathematics that has not been automated either.\n\n### 4.2 Accepted before understood needs a checker\n\n**\"Alien\" names a state that exists only where something other than a reader does the checking.**\nThe kernel accepts a proof that no person follows. An experiment can confirm a prediction whose\ngrounds nobody understands. A forecast can come true. In each case the result stands first and\nunderstanding comes later, if at all. September's line here says the second half of that: checked\nis not yet understood.\n\n**The converse is what bears on this project.** For a weighing, a value, or the step from one claim\nto another, nothing outside a reader can settle the matter. An argument of that kind that nobody\ncan follow is not a truth waiting to be translated. It has no standing. The graph's fact leg\nsometimes has an outside check, which is what the horizon kind called empirical marks. The rest of\nthe graph does not.\n\n**The strength code already behaves this way.** A link that a machine drew between claims other\npeople wrote counts for nothing until its relevance is proposed with confidence or argued\n(`deliberus/relevance.py`; ruled 2026-09-28, ledger Q33).\n\n**So the post's first stage has no counterpart here.** In mathematics a proof may be tidied after it\nis known to be true. Here cutting a claim into parts, writing out a step and linking it to what\nexists are the acts that make any checking possible. That is the ground under the gate ruled on\n2026-09-21, that machine work is judged by whether it gives a reader more places to disagree\n([earning-the-right-to-write.md](earning-the-right-to-write.md)).\n\n### 4.3 The reward with its first term taken away\n\n**The post's reward has three terms: the proof compiles, it is shorter, it passes the style\nchecks.** The first is the anchor. A shorter and tidier proof that does not compile scores nothing.\n\n**Most of what Deliberus stores has no first term.** A pass scored on the other two would be paid\nfor two errors this corpus already tracks. Being paid for shortness is being paid for leaving\nthings out, and what summarisers leave out first is the rare argument\n([saturation-and-the-long-tail.md](saturation-and-the-long-tail.md)). Being paid for fitting the\nhouse style is being paid for forcing new material into the shapes already stored, which the\ncorpus calls frame lock-in and counts as one of two errors that only a person standing elsewhere\ncan catch ([the-residual-error-taxonomy.md](the-residual-error-taxonomy.md)).\n\n**Nobody here has proposed such a score.** It is written down because it is the natural one to\nreach for. Both terms are cheap to compute, and both look like quality.\n\n**The field itself moved off length while keeping its compiler.** Proof-Refactor argues that length\nis what can be measured and is not what a library needs. Lean Refactor notes that a shorter proof\nmay call heavier automation and cost more to check.\n\n**The style term also has no place for \"this does not fit the house\".** A proof that goes around\nthe library's concepts may be clumsy. It may also show that the library lacks a concept. The post\ntreats every such proof as material to translate. The corpus's rule for closed lists applies to\nany pass that files new material under stored rules, concepts or claims: it needs a way to say\n*none of these*, and a count of zero there is an alarm.\n\n### 4.4 Two kinds of shorter\n\n**A proof gets shorter in two ways.** One line can call a lemma that already exists. The reader can\nopen the lemma, so nothing is lost and one level of pointing is added. Or one line can hand the\ngoal to an automatic tactic. The kernel is satisfied, and the reasoning is no longer on the page.\nProof-Refactor counts the second as a fault. Lean Refactor counts both as gains in length.\n\n**Deliberus has the same pair.** A claim can point at a stored claim that carries its own support,\nwhich is reuse. Or a passage can be summarised, which removes the places a reader could have\ndisagreed. Where the corpus says of the map of horizons that the compression is the product\n([convergence.md](../convergence.md)), it is the first kind: each entry opens. The rule proposed\nfor agent surfaces says the same of anything shown to an agent (ledger AE3).\n\n**A word count cannot tell the two apart.** That is the exact reason length cannot be a target for\nany pass that rewrites what a claim says.\n\n### 4.5 Why a library can overwrite and a graph cannot\n\n**Mathlib renames, restates and moves its contents all the time, and removes an old name after some\nmonths.** That is safe because every use of a changed statement is checked again. A change that\nmatters breaks something loudly. Once nothing breaks, nothing depended on the old form.\n\n**Here nothing breaks.** When a pass rewords a claim, merges two or regroups their parts, every\nvote, objection and link that pointed at the old form now points at something slightly different,\nand no build fails.\n\n**So *contributions are added, never overwritten* does a second job.** It was ruled so that edit\nwars have nothing to run on. It also stands where the compiler stands. It cannot stop a bad\nrewrite. It keeps the rewrite visible and reversible. And an old form here can have no date of\nremoval, because nobody can show that no reader's vote meant it.\n\n**What can be checked in the compiler's place, with no person judging and no answer key, are\nproperties of the tidying. None of them is about truth.** The corpus holds each of the five\nsomewhere. Together they are a list for any pass that rewrites or regroups:\n\n1. Nothing the original said is gone. Code can check this for names, numbers and dates. For the\n   rest the splitter's coverage check does it, as a separate model call.\n2. Undoing the pass restores the earlier state. The step that replaces old splits has an undo.\n3. Running the pass again changes nothing. Asked of daemons, and of every pass's answers since\n   2026-09-29.\n4. The order of the inputs does not change the result. This is ledger T4, and it has been measured\n   as failing twice: 59% of the linker's candidate pairs depend on which source arrived second, and\n   a check on a written-out step changed with the order of two premises on 14 of 44\n   ([what-a-link-rests-on.md](what-a-link-rests-on.md)).\n5. Every rewritten form still points at the words it was made from. This is Arc AA's proposal, and\n   code can compute the pointer today for 923 of 1,144 extracted claims\n   ([store-the-uses-read-the-meaning.md](store-the-uses-read-the-meaning.md)).\n\n**Two limits** (added the same day, with a correction: the first version of this section said code\ncan check all five). A pass that does nothing passes all five. They cap the damage a tidying pass\ncan do and say nothing about what it gained. And they are not all laws for code in the Bend note's\nsense: the first needs a model's reading beyond names and numbers, and the third and fourth are\nchecked by running a pass twice and comparing, which holds only while a pass's judgements are read\nback from the record and not made again.\n\n**Software testing has a name for this.** A program whose single output cannot be checked against\nan answer is tested by relations between several runs: change the input in a known way and see\nwhether the output changes as it must. The field calls the missing answer key the oracle problem\nand the remedy metamorphic testing. One of its findings bears on this list: a few varied relations\ncaught faults about as well as an answer key did (§ 7).\n\n**The tidying research has the same division inside mathematics.** Beside the kernel's check of\neach proof it runs a separate check that the tidied version proves the same statement. The post's\nfifth technique is that check.\n\n### 4.6 How general a rule should be, with and without a prover\n\n**⚠ Read § 6b with this section.** The founder's questions the same day showed three things it\nmissed. Its contrast with a prover stands. Its account of where a rule comes from does not.\n\n**Mathlib asks for the widest statement that can be proved.** The prover makes width safe. A\nstatement that is too wide fails to prove and never enters. A statement that is too narrow enters\nand costs later, as duplicates and debt. So the pressure is all one way: widen.\n\n**Here nobody proves the rule under a link.** A rule worded wider than its link needs covers cases\nnobody examined, and one counterexample refutes it. A rule worded too narrowly fails to meet the\nother links it should serve, and reuse is lost. The cost of going wide is paid at the door there.\nHere it is paid later, by readers.\n\n**Proposed: the default is the narrowest rule that covers the links it serves, and a wider rule is\na reading somebody offers.** Rules are already kept in the plural, each with whose reading it is\n(ledger AD25). This gives the plural a first member and an order.\n\n**Proof-Refactor's order of work shows how to get it.** Its agent first cuts fragments out of each\nproof, in that proof's own terms. It groups fragments that look alike. Only then does it word one\nhelper per group, with the library's existing statements on the table. A fragment is temporary and\nnothing else may be built on it. For links that would be: write what each step needs in the case's\nown terms; group across links; then word one rule per group, looking first for a stored claim that\nalready says it (ledger AD18, *found before made*).\n\n**That fits what was measured here on 7 October.** The trial named a rule under each link and then\ngrouped the wordings, and grouping by wording merged whole topics below a similarity of 0.75\n(ledger AD10). Two writings of one link's rule agreed, or one contained the other, on 23 of 27\n([philosophy-of-the-unwritten-step.md](philosophy-of-the-unwritten-step.md) § 6): the second case\nis one rule at two widths. Under a single link the narrowest covering rule is the link said over\nagain, which raters in the outside reading rejected as an explanation. One link fixes no width.\n\n**With several links the width comes from the record.** Where the links of a group differ, the rule\nlets that term vary. Where they agree, the term stays in the rule. The links are each other's\nanswers to AD25's question, *would the step still hold if this term were that one?* Refused steps\npush the other way: a rule must not cover a step people reject (ledger AD27 shows each rule with\nits strongest counterexample).\n\n**Three cautions from the corpus.** Only links that a text or a person drew count as such answers:\nten links one machine drew are one reader's habit. What everybody assumes recurs most, so the count\nis conservative. And a rule can be made wide enough to say nothing\n([what-a-rule-rests-on.md](what-a-rule-rests-on.md)).\n\n**The step that cannot be borrowed is the third.** After designing a helper the agent proves it, and\na wrong helper never reaches the last phase. Here a wrong rule is caught by a reader or a\ncounterexample, later. The stand-in on file is AD17: the rule is the machine's sentence and\nnobody's claim, and weighs nothing until a text states it or a person takes it up.\n\n*2026-10-10, later: he ruled that a machine's sentence under a link is a claim from the moment it is written (\"The moment it's written. Go ahead and make it happen.\", ledger AG12). So where this says* nobody's claim*, read* a claim nobody asserts*. That it weighs nothing, and how it is shown, stand as written.*\n\n### 4.7 A test with a known answer\n\n**The tidying field makes its own test pairs.** It takes a short clean proof, has a model expand it\ninto a clumsy one, and keeps both. A tidier can then be tried on problems whose good answer is on\nfile (Lean Refactor; an earlier system trained on such pairs, by that paper's account).\n\n**The pass that writes out the unwritten rule under a link can be tested the same way.** Some\nauthors state their own rule. Hide that sentence, give the pass the link, and count how often what\nit writes is the author's rule or contains it. The author wrote the answer before the test\nexisted, so the test cannot be tuned to the pass.\n\n**It measures recovery and not correctness.** A step has several acceptable rules, so a pass can\nwrite a good rule that is not the author's. The corpus's outside reading holds two relatives of\nthis test. Argument parts filled in by a model were rated below the originals. And within one\nnarrow pattern two annotators wrote the same missing premise in 69 of 71 cases, which suggests the\ntest will read well only where the kind of step is narrow\n([outside reading](writing-out-the-unwritten/outside-reading-explication-with-checks.md)). The\nfirst step is a count that has not been made: how many links in the stored sources have a rule\nthat their own text states.\n\n### 4.8 Review that teaches nobody\n\n**Mathlib's guide gives the reason its reviewers resent machine-written submissions.** A review is\npartly teaching. When no person is learning from it, the effort improves nothing that comes later.\n\n**That names the condition under which reviewing machine work pays: what the reviewer finds must\nreach whatever produced the work.** For Deliberus's own passes it can. The project owns the\ninstructions, and the canon says a fault found changes the instruction. It holds only while the\nnotes are read, and today one script reads them and no page shows them\n([the-evals-loop-and-our-machine-passes.md](the-evals-loop-and-our-machine-passes.md)).\n\n**For work written by outside agents it could not.** Their instructions belong to somebody else.\nThat is a third reason for the standing position that agents read and do not write, beside the two\non file: no defence against many accounts posing as independent sources, and the ground of the\ngraph staying human ([agents-as-a-consumer-class.md](agents-as-a-consumer-class.md)).\n\n**A small thing to copy.** The library asks that machine-written code be labelled, on the ground\nthat tools make other mistakes than people do, so a reviewer knows what to look for. The marks here\nsay who wrote a thing and what it may weigh. They could also open the pass's known faults. The\nreview of machine-cut parts already does this for one fault of the splitter\n([the-parts-review.md](the-parts-review.md)).\n\n### 4.9 Where the queue forms\n\n**Mathlib has one current text and a gate in front of it.** Nothing enters unreviewed, so the queue\nstands at the door. Its guide tells projects that want to move fast to live outside the library and\ndepend on it, so fast work forms a ring around a slow core, and reaches the core only through the\nsame gate.\n\n**Deliberus ruled the other way on existence.** Nothing needs permission to exist. What is gated is\nweight, and which form of a thing is shown first. So the queue here stands at the review of what\nmachines wrote, and the ring and the core are staged maturity and the community compartments\n([blobs-community-sandboxes-and-the-advice-process.md](blobs-community-sandboxes-and-the-advice-process.md)).\n\n**Both designs have the same unsolved step: moving a thing inward.** There it is called\nupstreaming, and the post's whole proposal is to automate it. Here [vision.md](../vision.md) has\ncalled it promotion and left it open since April. This reading adds two things to that open\nquestion. Promotion has to add and point back, for the reason in § 4.5. And its unit should be\nsmall enough to judge at a glance, one rule with its links or one merge, because judgement is what\nthis step spends.\n\n### 4.10 Tidying that changes the statement\n\n**The post's fifth technique guards against a tidier that quietly alters what a lemma says.** The\ncorpus has measured its own version. Across 1,144 extracted claims, 29% of a claim's content words\non average appear nowhere in its source, with a median of 20% (ledger AA6). And the author of one\nmapped text read his map in September and found that what he had marked as assumptions read as\nthings he knew\n([mapping-a-structured-position-on-ai-governance.md](mapping-a-structured-position-on-ai-governance.md)).\n\n**In mathematics the guard is to compile both versions against one statement.** Here the guard on\nfile is Arc AA: store the author's passage as a pointer, and treat any rewording as a dated\nrewrite. This reading is outside support for it. The less a tidy form replaces and the more it\npoints, the less there is to drift.\n\n---\n\n## 5. Where the comparison breaks\n\n- **What the first stage produces there is true. Here it is asserted, by somebody.** Everything in\n  § 4 about tidying carries over. Nothing about the raw material does.\n- **A library has one community's manner. Here the manner is itself in dispute.** One group's\n  natural way to cut a question is another group's bias, so \"rewrite it in the house style\" has no\n  single target. The corpus's answer is to keep the lenses plural\n  ([worldview-lenses.md](../worldview-lenses.md)).\n- **Nobody gains from a false lemma, because it cannot be proved.** People do gain from which\n  wording of a claim becomes the standard one. No instrument here has yet met a person with a stake.\n- **A proof's tidy form can replace its clumsy form with no loss. A person's words cannot be\n  replaced by a tidier version without their say.**\n\n---\n\n## 6. Proposals\n\nAll unruled, and all in the ledger as Arc AF.\n\n| # | Proposal | Why now |\n|---|---|---|\n| AF1 | For a step from a general statement and a case, the general sentence a machine writes is a guess that a group of links prompts. It starts no wider than those links, widens as far as a stated mechanism reaches, and narrows at each case that breaks it. A sentence drafted under one link is a draft that nothing hangs on. *(Revised the same day, § 6b.)* | § 4.6, § 6b. Sharpens AD10, AD18, AD25 and AD27. Try it by hand on the thirty links of 7 October before building. |\n| AF2 | Any pass that rewrites or regroups is held to five tests that no person has to judge and that need no answer key, before anyone samples its judgements: nothing lost; undo restores; twice is once; any order, one result; the original is still pointed at. | § 4.5. Collects T4, the Bend note's laws, the coverage check and the undo paths in one list. One of the five is measured as failing, twice. They cap damage and do not show gain. |\n| AF3 | No pass is rewarded for making what a claim says shorter, or more like what is stored. A pass may shorten only by pointing at something a reader can open, and it reports what refused to fit beside what it reused. | § 4.3, § 4.4. A reading rule for any figure a pass reports. |\n| AF4 | The pass that writes out a link gets a test with a known answer: hide a rule the text states, and count how often the pass writes it back. | § 4.7. Count the stated rules first; run it if there are fifty or more. |\n| AF5 | Where a machine-written item is shown with its mark, the mark opens that pass's known faults as readers found them. | § 4.8. Small, and for when the marks are next touched. |\n\n### 6a. Sharper on a second pass, the same day\n\n- **AF1, going wider later is cheap here.** A library that starts narrow pays for a refactor when\n  it widens, because every user of the old statement has to be moved. Here the narrow rule stays\n  and the wider one is added above it. So the two fields differ twice: no prover makes width safe\n  here, and no refactor makes narrowness costly.\n- **AF1, *narrowest* depends on which kinds the vocabulary has.** A squirrel and a fox that both\n  smell of decay are covered by *an animal that smells so is dead*. Where no such kind exists, the\n  narrowest rule is a list of the cases, which says no more than one link said again. This is the\n  problem the philosophy note holds from Goodman\n  ([philosophy-of-the-unwritten-step.md](philosophy-of-the-unwritten-step.md) § 6). The proposal\n  bounds it from below and does not solve it.\n- **AF1 is the founder's thought of 8 October as an order of work**: the cases first, and the rule\n  drawn from comparing them ([what-a-rule-rests-on.md](what-a-rule-rests-on.md)).\n- **AF3, reuse is the figure most likely to be turned into a score**, because reuse is what makes\n  the next mapping cheaper. The proposal is to count it and show it beside what refused to fit. The\n  map view is the model for the other half: it shortens by showing about ten boxes that each open,\n  and it says what kind of thing it left out.\n- **AF4 is best used to compare two ways of writing rules on the same hidden sentences**, for\n  example today's order against AF1's. A comparison survives the fact that a step has several\n  acceptable rules. Two limits: authors state the rules they expect to be disputed, so stated rules\n  are not typical of unstated ones, and the text around a hidden sentence may give it away.\n- **AF5 needs nothing new to be made.** The list of a pass's faults is what reading the pass\n  produces, in the order ruled on 2026-10-06. Shown beside the mark, it is the confession principle\n  applied to each pass, and it gives the reader a move: what to check.\n\n### 6b. The first proposal after the founder's questions, the same day\n\n**His words**, on hearing the first proposal with the squirrel as its example: *\"There are many\nintermediate reasoning steps in that link chain, no?\"* · *\"Did you take full account here of\neverything that is accounted for in the last audio walkthrough generated\"* · *\"I feel like there's a\nclear place here for mechanistic evidence about WHY decomposition occurs\"* · *\"What would a \"prover\"\neven be, in the context of Deliberus?\"*\n\n**The answer to the second was no.** The walkthrough of 8 October\n([what our own notes already knew](../listening/2026-10-08-what-our-own-notes-already-knew.md)) was\nread only after he asked. Three things in it, and in the notes under it, had been missed.\n\n1. **The squirrel is a step from a sign, and such a step has no general rule whose width could be\n   set.** What is written under it is the law that runs from the thing to its sign, *dead squirrels\n   smell of decomposition*, which is his own sentence of 2011, and the question what else would\n   produce the sign here\n   ([philosophy-of-the-unwritten-step.md](philosophy-of-the-unwritten-step.md) § 5). The example\n   given to him in chat was the converse, *squirrels that smell so are dead*, which that section\n   calls the sentence a person seldom gives as their reason. Of the 443 links whose kind falls under\n   the four shapes, 206 go from a general statement and a case\n   ([what-a-rule-rests-on.md](what-a-rule-rests-on.md) § 6). The proposal speaks to those.\n2. **A rule is a guess that its cases have not yet broken.** Cases prompt the guess and cases test\n   it. § 4.6 read the rule off its cases, as the narrowest sentence that covers them.\n3. **Grouping links is a judgement of likeness, and a machine's likeness is everyone's average.**\n   § 4.6 named grouping as a judged step and missed this. A group therefore says in what respect\n   its links are alike.\n\n**Where the mechanism goes.** In three places. It is the chain inside the law: the animal dies, its\ndefences stop, bacteria break the tissue down, and what they release is what is smelled. Each of\nthose is a step somebody can open and dispute, which is his first remark. It answers the question a\nstep from a sign leaves open, because knowing how the smell is made says what else could make it.\nAnd for a step from a rule and a case it says how far the rule may reach: as far as the mechanism\noperates. The evidence note already proposes mechanistic evidence as its own stream, beside\nevidence from cases ([what-counts-as-evidence.md](what-counts-as-evidence.md); ledger Q8, unruled).\n\n**The proposal as revised** is in the table above and in the ledger. Its form (every wording\nkept, two shown), and the answer to his next question, when the machine writes, widens and narrows\nand on what, are in [the-chain-inside-a-link.md](the-chain-inside-a-link.md). The contrast with the library\nis kept and made sharper. A prover licenses width there. Here the nearest licence for width is a\nmechanism, and the nearest check is a case that breaks the rule, found in a text or brought by a\nperson.\n\n**What a prover would be here.** A prover says of one step that it follows, with nobody judging,\nand refuses a statement that claims too much. The corpus answered in March that a checker of this\nkind could check form and never truth\n([lean-deliberus-analogies.md](lean-deliberus-analogies.md), the table of what a kernel can and\ncannot check). October gives that table two updates. Its row for deductive steps has a first built\ninstance: a reader that is given the written sentences, is not told that a conclusion was drawn,\nand says what follows. It gave the same answer in both orders on 26 of 29 steps, and it refuses the\nsquirrel. Its row for relevance was measured and failed: a machine's yes or no on whether one claim\nis a reason for another changed with the wording of the question on eighteen of thirty links\n([what-a-link-rests-on.md](what-a-link-rests-on.md)). So, by kind of step: for a step from a rule\nand a case, that reader. For a step from a sign, the world, by ruling out what else would produce\nthe sign. For a weighing, nobody. What exists here says no far better than it says yes.\n\n---\n\n## 7. What was read outside the post, and how far\n\n| Source | Read |\n|---|---|\n| *Contributing to mathlib*, the library's guide (leanprover-community.github.io/contribute), as it stood on 2026-10-10; its own wording dates it mid-2026 | the page, directly |\n| Baanen, Ballard, Commelin, Chen, Rothgang, Testa, *Growing Mathlib: maintenance of a large scale mathematical library*, arXiv:2508.21593, August 2025 | abstract and opening directly; the two counts through a reader |\n| Ahuja, Avigad, Tetali, Welleck, *ImProver: Agent-Based Automated Proof Optimization*, arXiv:2410.04753, October 2024 | abstract directly; one sentence through a reader |\n| Lu, Kong, Stehling, Yang, Wang, Sun, Chen, *Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search*, arXiv:2605.20244, May 2026 | abstract directly; four passages through a reader |\n| Fu, Liu, Wang, Yuan, *Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts*, arXiv:2606.03743, June 2026 | abstract and opening directly; five passages through a reader |\n| The post, its image and its six comments | in full |\n| On testing with no answer key: Segura, Fraser, Sanchez, Ruiz-Cortés, *A Survey on Metamorphic Testing* (IEEE TSE 2016); Barr, Harman, McMinn, Shahbaz, Yoo, *The Oracle Problem in Software Testing: A Survey* (IEEE TSE 2015); Liu, Kuo, Towey, Chen, *How Effectively Does Metamorphic Testing Alleviate the Oracle Problem?* (IEEE TSE 2014) | abstracts and search extracts |\n\nA reader that answers questions against a page can misquote. Check these against the papers before\nciting any of it outward.\n\n---\n\n## See also\n\n[formalized-fermat-and-the-oracle-boundary.md](formalized-fermat-and-the-oracle-boundary.md) ·\n[understanding-after-the-proof-machines.md](understanding-after-the-proof-machines.md) ·\n[bend-and-deliberus.md](bend-and-deliberus.md) ·\n[lean-social-system-research.md](lean-social-system-research.md) ·\n[the-reuse-flywheel-prior.md](the-reuse-flywheel-prior.md) ·\n[writing-out-the-unwritten.md](writing-out-the-unwritten.md) ·\n[philosophy-of-the-unwritten-step.md](philosophy-of-the-unwritten-step.md) ·\n[store-the-uses-read-the-meaning.md](store-the-uses-read-the-meaning.md) ·\n[earning-the-right-to-write.md](earning-the-right-to-write.md) ·\n[proving-a-pass-reliable.md](proving-a-pass-reliable.md)\n"}