Protocol: how the pool of both passes was built

Every search, count and rule of the review, run on 2026-10-29: the grey pass, one reviewer per side, then the formal pass, one reviewer per strand, all merged. Terms are defined in frame; the pool is in sources. Shared rules of the family: evidence README.

Shape: protocol

1. Why grey literature

Garousi 2019, Table 4, answered by each side: seven of seven questions get a yes on both.

# Question Formal side Human side
1 Complex, not solvable from formal literature alone? yes: blueprints, comparator, registries and editor tools come from practice yes: the workflows changed month by month in 2025 and 2026; papers lag
2 Lack of volume or quality of evidence? yes: tools change monthly; no grey source measured guidance for a person yes: this pass met no controlled study of the loop
3 Context important? yes: competition problems against research papers; teaching against research yes: research, teaching and benchmarks; experts and novices
4 Corroborate research with practice? yes: benchmark scores against what practitioners check yes
5 Challenge practice with research, or the reverse? yes: compile rates against statement fidelity yes: reports disagree on whether formalizing helps understanding (review Q4)
6 Would a synthesis serve both communities? yes yes
7 Large practitioner volume? yes: the public forum archive lists 9,893 topics in its general channel alone yes: 5,053 pull requests in Formal Conjectures at this side's count (5,054 at the audit later that day) and 1,399 in PNT+ (GitHub 2026f, 2026g); 482 topics in one forum stream (P4)

2. Questions

The scope's five questions, Q1 to Q5 of frame: prior art, translation, feedback, form, limits. The frame maps each side's sub-questions (F1 to F5, H1 to H4) and each formal strand's (A1 to A4, C1 to C7, and strand B's parts of Q1 and Q3) onto them.

3. Existing reviews

  • Neither side found a grey review of the whole loop.
  • Formal side: two grey overviews of practice were found and used, Hales 2026 and Avigad 2026. One practitioner answer catalogues the checks for a wrong statement, PASE 2026. One formal survey was met and listed, on proof assistants for teaching.
  • Human side: two formal surveys were met by citation and listed among the formal leads, not read; the formal pass screened them (section 4).
  • Held by the family, linked and not repeated: structured proofs and blueprints (reader-ergonomics-academic, mathematical-writing); prose linting and docs as code (reader-ergonomics-topic, document-model).
  • Formal pass: each strand searched for existing reviews before its other strings (section 4); the reviews found are in review, section 0.

5. Grey search, formal side

  • Types: tool repositories and documentation, because the tools are the practice; the Lean reference and release notes, the checker's account of its own feedback; company pages, as their owners' claims.
  • Producers: the practitioners who run the largest projects (Tao, Buzzard and their guests), who report workflows; the Lean community forum's public archive and Q/A sites, for practitioners' own questions.
  • Engine: a general web search engine, first result page per string, no login. Results personalise and change.

Web strings

Id String as run Shown Included
G1 Lean blueprint projects list leanblueprint dependency graph formalization 10 0 (papers only, to leads)
G2 autoformalization Lean tool natural language statement to Lean 4 9 2 (StepFun 2025, Numina 2025)
G3 controlled natural language proof checker Naproche ForTheL 9 0 (papers; site visited, P)
G4 Lean 4 error messages explanations improve readability error explanation 10 2 (Lean FRO 2025, 2026c)
G5 Lean Verbose Massot controlled natural language Lean tactics teaching 10 1 (Massot 2026b)
G6 Isabelle Isar readable structured proof language what it asks of the writer 9 0 (manuals timed out; P)
G7 Lean Copilot LeanDojo suggest_tactics LLM proof automation README 10 1 (LeanDojo 2026)
G8 Terence Tao blog Lean formalization AI tools experience 9 0 (secondary only)
G8b terrytao.wordpress.com Lean AI formalization equational theories project (restricted to that site) 9 1 (Tao 2024)
G9 Kevin Buzzard Xena blog AI Lean formalisation Fermat's Last Theorem blueprint 9 1 (Anthropic 2026c)
G10 Harmonic Aristotle Lean autoformalization formal verification claims 19 2 (Harmonic 2024, Rivin 2026)
G11 LLM explain Lean error message beginner feedback tool 9 0 (none on Lean; C and Python papers to leads)
G12 leanblueprint checkdecls GitHub Actions CI blueprint docgen-action 9 1 (Zhu 2026)
G13 Waterproof Coq Rocq students natural language proofs feedback Eindhoven 20 1 (TUe 2026)
G14 Math Inc Gauss autoformalization agent strong prime number theorem Lean 10 1 (Math Inc 2025)
G15 Lean 4 hint tactic exact? apply? suggestions try this guidance 29 1 (Lean FRO 2026d)
G16 Diproche automated proof checking students natural language feedback Carl 10 0 (papers to leads)
G17 Lurch word processor checks mathematical reasoning natural language proofs 10 1 (Lurch 2026)
G18 lean-lsp-mcp Lean language server MCP agents diagnostics goals 9 1 (Dressler 2026)
G19 Formal Conjectures Google DeepMind repository misformalization review open problems Lean 28 1 (Google DeepMind 2026)
G20 Leanstral Mistral Lean prover agent release 19 1 (Mistral 2026)
G21 AxiomProver Putnam (2025) Lean formal proofs Axiom Math claims 19 1 (Axiom 2026)
G22 tool translate Lean proof into natural language explanation informalization 10 0 (papers to leads)
G23 blueprint LLM agents formalization workflow informal blueprint written by mathematicians AI fills Lean 28 0 (papers to leads)

Total: the 24 strings above showed 323 results in all, and 19 were included.

  • G8 returned only secondary coverage, so it was rephrased (G8b) and followed by the blog's tag pages (P).
  • G11 returned nothing on Lean in three phrasings (G11, G15, G22); Lean-specific guidance was found by producer visits.
  • The engine's answer text was used only to find pages; every number was read on the page itself.

Producer visits (P)

Producer Pages read Included
leanblueprint repository README, public metadata Massot 2026 (carried key, re-read)
Tao's blog three tag pages (11 posts listed), 5 posts read Tao 2026e, Tao 2026f, Hales 2026
Xena blog front page (10 posts listed), 3 posts read Buzzard 2026a, Buzzard 2026b, Avigad 2026
Palomar registry About, Statement, How to submit, public data API Palomar 2026; a count
Lean FRO comparator README; release notes 4.35.0 Lean FRO 2026a, 2026b
Mathlib Initiative formalization.yaml README and template Mathlib Initiative 2026
Naproche, Isabelle project site and tutorial; overview page Naproche 2026, Isabelle 2026
Lean community lean4game documentation; mathlib statistics page Lean-community 2026; a count
Model cards DeepSeek-Prover-V2, Goedel-Prover-V2 DeepSeek 2025, Goedel-LM 2025
Tool repositories LeanAide, LLMLean, LeanTool Gadgil 2026, CMU L3 2025, GasStationManager 2026
Forum archive 8 channel indexes, 24,928 topic titles filtered by keyword, 126 matched, 4 threads read Vergo 2026; one thread to the other side (LZ 2026b here)

Q/A sites

Stack Exchange API 2.3, search/advanced, sorted by votes, 30 per page, no key, no login.

Site Strings as run Returned = screened Included
Proof Assistants q=autoformalization 2; q=blueprint 3; q=controlled natural language 0; title=natural language 2; title=readable 0; title=error message 0; q=Naproche 0; q=Isar readable 1; q=Verbose Lean 4; title=declarative 0; title=error 28; q=human-readable proof 5; q=natural language proof 19; q=Mizar 15; q=LLM 3; title=AI 0; q=structured proof 30; q=hammer suggest 0 112 3 (PASE 2022, 2024, 2026)
MathOverflow q=autoformalization 2; q=blueprint Lean 0; q=Lean formalization AI 11; q=controlled natural language 9 22 1 (MathOverflow 2026)
  • Zero-result strings were rephrased in title and body forms before concluding.
  • Display names are recorded only for answerers whose answer is used, as the platform shows them.

6. Grey search, human side

All on 2026-10-29. No login, no key, no identity sent; public interfaces only.

Type Producers Why
practitioner blogs the Xena Project blog (Imperial College); Terence Tao's blog; two blogs reached by snowball the people who run the largest projects write here first
microblog posts Terence Tao's public Mathstodon account his journal of each workflow, often with times and line counts
community forum the Lean Zulip public archive where practitioners report failures and propose checks
project documentation Formal Conjectures, PNT+, the Erdős problems database and wiki, comparator, Verbose Lean, an audit repository the rules projects actually enforce, and counts
Q/A site Proof Assistants Stack Exchange voted answers
company and organiser pages Google Research, the STOC 2026 organisers, PostHog model feedback on writing, as claimed by its owners
talks one seminar abstract a named failure mode

Web strings (a general web search engine)

Id String as run Seen = screened Included
W1 Terence Tao Lean formalization GitHub Copilot experience blog 18 0; led to P3
W2 misformalization Lean statement proved wrong version AI Erdős problem 36 0 new; led to Alexeev 2025 and P5; 5 formal leads
W3 Kevin Buzzard Xena blog AI formalization Lean 9 0; led to P1
W4 tadamcz formal conjectures language model audit misformalizations review results 9 0; led to Adamczewski 2026; 2 formal leads
W5 erdosproblems.com forum guidelines AI-generated proofs Lean check main statement accuracy 9 0; led to Erdős DB 2026
W6 Terence Tao YouTube "Formalizing" Lean AI tools video workflow autoformalize equational 18 0; 1 formal lead
W7 STOC 2026 Gemini automated feedback experiment results survey authors found helpful 18 Google 2025, STOC 2026; 2 formal leads
W8 LLM documentation linter in CI pull request style guide Vale comparison practitioner write the docs 27 PostHog 2026
W9 "vibe proving" Lean experience report blog mathematician what worked what did not 36 Tanswell 2026; 1 formal lead

Producer visits

Id Producer and route Listed Opened Included
P1 Xena Project blog, public WordPress API, 60 latest titles 60 7 7
P2 Tao's blog, public WordPress API, searches Lean, formalization, AI tools, Aristotle, equational theories 83 (with repeats) 8 4
P3 Tao's Mathstodon, public Mastodon API, 1,000 statuses back to 2022-12, keyword filter 32 matched 14 read in full 8
P4 Lean Zulip archive: stream indexes filtered by title (Machine Learning for Theorem Proving 482 topics, Lean for teaching 171, general, mathlib4, PR reviews) 117 matched 9 read, 1 failed 9 (4 below 10)
P5 GitHub, public API without a token: Formal Conjectures, an audit repository, comparator, PNT+, the Erdős database, Verbose Lean 11 repositories 10 documents 7, plus 3 counts
P6 snowball from P3 to Kirov's blog, then to Paulson's blog 2 indexes 6 3
P7 Proof Assistants Stack Exchange, API 2.3, search/advanced, order=desc&sort=votes&pagesize=30 72 2 1
  • P7 strings: q=autoformalization 2, q=LLM 3, title=formalization 9, q=blueprint 3, q=language model 16, q=statement faithful 0, q=structured proof 30, q=junk value 0, q=misformalization 0, q=wrong statement 9.
  • Four of them first failed on an encoding error and were rerun in the forms listed.
  • Zero results were read as a weak query; the same idea was then run in another form.

Read again at the merge

  • The brief allowed the web again only to settle a conflict between the two sides. Two pages were read once more, on 2026-10-29, without saving them.
  • Hales 2026: the sides placed its audit sentence in different sections; the page has the part Lean's design inside the section Is Lean reliable?, so both were right.
  • Massot 2026b: the sides gave different contrasts for Verbose Lean's aim; the README's first paragraph says not easier to write.

7. Stopping rule

  • Stated in the brief before searching, for both sides: top 10 per web string; stop after 5 consecutive results that add no concept; Q/A, top 30 by votes.
  • Formal side: every lead of the brief was run, in three forms where the first found nothing; results beyond 10 came from the engine's follow-up pages and were screened by title. The run ended after G22 and G23 added only papers and no new practice concept.
  • Human side: web strings returned lists of 9 links, and every title in a list was screened; each producer listing was read in full by title.
  • Human side: opening stopped when each of H1 to H4 had at least three sources scoring 10 or more. The last five opened (LZ 2025d, LZ 2025g, LZ 2025h, two snowball posts) added no concept.
  • Formal pass, stated before searching: effort bounded, with saturation at 5 consecutive titles adding no concept.
  • Strand A: the 15 most cited Semantic Scholar results per string, and every arXiv title returned, up to 34 per string.
  • Strand B: the 15 most cited Semantic Scholar results and the first 10 arXiv results per string; evidence exhaustion for F2, F3, F9, F10, F21 and X1 to X5, whose sets are small.
  • Strand C: the 15 most cited results per string, with evidence exhaustion for strings under 20 results.

8. Selection

  • Formal side, include: a source on joining informal mathematical writing to a proof assistant, on translating it, on checking the translation, or on turning a checker's output into guidance. Include also a company's account of its own prover, labelled as its owner's claim.
  • Formal side, exclude: papers (listed as leads); news coverage of a primary page that was itself readable; opinion threads with no practice or data; duplicates.
  • Human side, include any of: a report of practice where a person works with a model or a proof assistant on reasoning a person wrote; a wrong formal statement caught, and how. Also a check of writing in CI with a model in it, or a report on whether splitting reasoning helped thinking.
  • Human side: English, dated or datable, readable without login on the search date.
  • Human side, exclude: news rewrites, mirrors and aggregators (about 25 links: secondary); product pages on prover capability (to the formal side); formal papers (to the leads); Vale-in-CI pages already held by document-model (3).
  • Both: a page that could not be read is reported in section 11 and never used.
  • Formal, strand A, include: papers and preprints with a result or an argument on translating informal mathematics into a proof assistant. Its measurement, its error rate, and the detection of wrong statements count, as do existing reviews of these.
  • Strand A, exclude: provers evaluated only on supplied formal statements (their scores are in review Q2); translation into first-order logic, law or software specifications, unless a method transfers (none was kept). Also long-horizon case studies with no measure of faithfulness (LeanMarathon, Landau damping, MIP* = RE, tensor networks).
  • Strand B, include: a paper, thesis or preprint with results on a structured informal-to-formal workflow, a CNL or a declarative proof language for mathematics.
  • Strand B, include also: results on error messages, proof repair, or explanations of a checker's output, preferably measured on people. Programming error-message studies with people are included as the nearest measured evidence, marked by language.
  • Strand B, exclude: program verification with no user or feedback content; formalizations of single theorems; statement translation and faithfulness (strand A); learning outcomes and teaching studies (strand C). Works readable by title only stay out unless they name a system the strand must place, and then they are marked "title and venue only".
  • Strand C, include: a study, review or argued paper on a person who writes or reads reasoning in a proof assistant, or with a model and a checker. Its subject is learning and transfer, use of the verdict, research practice, trust, the formal and informal gap, over-reliance, or cost. Reviews and controlled studies of over-reliance outside mathematics are included where no study inside it exists.
  • Strand C, exclude: prover and translation performance (strand A); error messages, repair and tool usability (strand B); verification of software except measures of cost; off-topic matches.
  • All strands: a work whose text and abstract could not be read is listed as located only, never as support.

9. Quality of sources

  • The 20 criteria and the threshold: evidence README.
  • A count read from a public listing (stars, downloads, registry totals) is the reviewer's measurement, not a source, and is not scored.
  • Formal side, outlet tier: project documentation, company pages, model cards, forum and Q/A pages, tier 2 (0.5); blogs and gists, tier 3 (0); no tier 1 source was found.
  • Formal side: a company page scores low on objectivity, as it reports its own success. Q/A authority is 0.5 for the site, plus 1 for an answerer at or above 20,000 reputation, 0.5 at or above 5,000.
  • Human side, outlet tier: project documentation, Q/A, company and organiser pages, talk abstracts, tier 2 (0.5); blogs, microblog posts and chat threads, tier 3 (0).
  • Human side: A1 is 0 for a personal blog, 0.5 for a moderated forum or site, 1 for an institution; a company page about its own tool scores 0 on O3 (vested interest).
  • Human side, impact 1 or 0.5: blogs, 30 comments or 10; Mathstodon, 50 favourites or 10; repositories, 500 stars or 100. Chat threads, 50 messages or 15; Q/A, the shared rule, 30 votes or 10.
  • Formal sources are graded, not scored. "measured" means a controlled study, a meta-analysis, or a benchmark with a stated protocol, said which.
  • "measured, descriptive" or "measured, qualitative" means counts, logs, surveys or coded interviews, with no comparison group.
  • "supported with caveat" means evidence with a stated limit, such as self-selected groups; "convention" means argued, proposed or reported by an owner, untested.
  • "not graded" marks a work read by title and venue only; "located only" a work whose text and abstract could not be read.
  • A benchmark number is measured on that benchmark only, with its split, its metric (pass@k, or the judge used for faithfulness) and its budget.

10. Extraction, synthesis and merge

  • Extracted per source by both sides: producer, date, the practice, the claim, any number with where it sits in the source, and whether the number is the source's own.
  • Each side wrote its synthesis by its own sub-questions; the merge reorders every finding by Q1 to Q5 in review, each with its key and where.
  • Keys: one key per work across both sides. Where the sides used different keys for one work, or one key for two works, the formal side's key is kept. That side had already checked its keys against the five bibliographies of the family.
  • Keys were then checked by script against the bibliographies of reader-ergonomics-topic (branch and master), reader-ergonomics, reader-ergonomics-academic, reader-ergonomics-presentations and reader-ergonomics-software-design. A key used there for another work took the next free letter; a work already there kept its key. The renamed keys are listed in sources.
  • Scores: a source scored by both sides keeps the score of the side that read more of it. That is judged first by the pages read, then by the parts of the source each side cites; the other side's score is given in its row.

Formal pass

  • Extracted per source by each strand: the design, the sample or benchmark, the metric, the judge of faithfulness (person, model or program), the number, and the section where it was read. Synthesis is narrative, by sub-question.
  • Each strand was then audited by someone who had not written it: every line carrying a number, or graded measured, checked against its primary source, and the counts of its protocol checked by arithmetic.
Strand Rows Correct Imprecise Wrong Unverifiable Checked before, or repeats
A 81 63 10 1 0 7
B 95 66 15 1 0 13
C 94 68 11 1 0 14
all 270 197 36 3 0 34
  • The three wrong rows: a comparison of two translators (three at one sample) given as five; a screened count of strand B (1,023) that its own rule makes 1,013.
  • And strand C's recorded exclusions, which cannot follow from its rule (584 titles).
  • Every wrong and imprecise row was corrected before the merge: budgets and metrics added to benchmark numbers, grades lowered where above their evidence, "(secondary)" added to abstract reads.
  • Four works that strand B had read by abstract, behind a paywall, were read afterwards in full through the university library: Wang 2024b, Hentschel 2016, Aitken 2000 and Becker 2019. Their rows give the full texts' numbers.
  • The merge: one key per work across the strands and the grey pass, checked against the family's six bibliographies.
  • A key used there for another work took the next free letter, so Draft, Sketch and Prove is Jiang 2023c.
  • A work met by two strands has one row in sources, its two routes joined, with the grade of the strand that read more of it.
  • Its numbers were checked to agree across the merged files.
  • Where an audit and a strand still disagreed at the merge, the audit's reading was kept.

11. Limits

  • One reviewer per side; no second rater on this pass. The six sources both sides scored are the only overlap, compared in sources.
  • Formal side: the Isabelle documentation server timed out on the Isar reference manual and the programming tutorial; Isar is covered by its overview page and by Wenzel 1999, held elsewhere.
  • Both sides: the forum's public archive stops at 2026-02-28; later threads were not seen. One topic whose link holds # returned 404 (human side).
  • Formal side: the unauthenticated GitHub search API hit its rate limit once, so the list of most-starred blueprint repositories was not read.
  • Videos and talks were located but not watched. The video site served the human side a consent page, so claims about Tao's videos rest on his posts. Social media posts other than Tao's Mathstodon were not read.
  • Human side: the audit site is rendered by script, so its repository data were read instead; Mastodon search needs a login, so the public timeline was paged and filtered instead.
  • Human side: the web archive's lookup service answered HTTP 429 on the day, so its sources have no archived copies; the formal side linked archived copies where it found them.
  • Pages carrying text addressed to automated readers were read as data only.
  • Formal side: no PDF was read in this pass.
  • Search engines personalise and change; counts on GitHub, PyPI, Palomar and Stack Exchange are those of 2026-10-29, and two moved the same day (Palomar 2026b, GitHub 2026f).

Formal pass

  • One reviewer per strand; no second rater on screening or extraction. The audits checked numbers and grades, not the screening.
  • Strand A: full texts were read in the arXiv HTML version, by section, never whole; a number outside the sections read was not seen. Most included works are 2025 and 2026 preprints; venues are given where arXiv or Crossref states one.
  • Strand A: Semantic Scholar refused three calls with rate limits; each was rerun once, and the rerun's count is given.
  • Strand B: Semantic Scholar refused many calls (429), so one acronym cell failed and five forward lists were not run. Per-reason exclusion counts were not kept.
  • Strand B: at the search, the ACM Digital Library and one university repository refused automated reads (403, 405). Aitken 2000, Hentschel 2016 and Wang 2024b were then read by abstract; the university library read came later (section 10).
  • Strand C: the Semantic Scholar counts of L1 to L10 came late or not at all (section 4).
  • arXiv refused strand C's calls for a few minutes (429), and the ten strings were rerun after a pause.
  • Strand C, behind a paywall, listed and not used for numbers: Hanna 2021, Knobelsdorf 2017, Avigad 2019, Nipkow 2012, Harrison 2006, Pierce 2009, Tymoczko 1979, Rav 1999, Tanswell 2015.
  • Matichuk 2015 is behind a paywall too; its abstract numbers are used, marked secondary.
  • Strand C: Hanna 2024 was read in its author copy, found through OpenAlex. Iannone 2025a was not reached, since the publisher's page asked for a browser check; OpenAlex lists an open repository copy.
  • Strand C: 17 works were found from memory and then verified, a bias toward known work, offset only partly by the strings.
  • In the university queue, still to be read: Knobelsdorf 2017, Tymoczko 1979 and Avigad 2019.
  • The strands saved no PDF or page; texts were read in memory. Text on pages addressed to automated readers was treated as data.

12. Second pass, 2026-11-03

Run on 2026-11-03, after the merge, on the review's three most cited keys and on its grey sources. Sections 1 to 11 are not changed; the additions are listed in sources and review.

Forward citations

The three keys cited most in review, counted with a word-boundary match over its text: Guo 2026b (10), Avigad 2026 (8) and PNT-plus 2026 (8). The next key has 7, so the three are fixed.

Key What it is Citing works, on 2026-11-03 Strings and screened numbers
Guo 2026b preprint, arXiv 2610.00760, posted 2026-09-30 (OpenAlex W7216044583) none: the OpenAlex cites: filter returns 0; Semantic Scholar's citations endpoint returns 0 OpenAlex title and abstract, since 2026-09-01: LeanSide 1 (itself); natural-language proofs Lean co-reasoning 1 (itself)
Avigad 2026 guest post on the Xena blog, 2026-10-16, no DOI not indexed: a blog post has no OpenAlex or Semantic Scholar record to be cited through Semantic Scholar title search: 802 results, the first page read, none is the post
PNT-plus 2026 project documentation, a repository file not indexed OpenAlex PNT+ blueprint, since 2026-01-01: 3 results, none about the project; not searched further

Strings run on OpenAlex's title and abstract field, each with a publication-date filter. The counts it returned:

  • autoformalization, since 2026-09-30: 25 results, all read by title.
  • Lean formalization natural language proof, since 2026-09-30: 14, all read by title.
  • formal conjectures Lean AI, since 2026-09-30: 80, the first 25 read by title.
  • blueprint Lean, since 2026-09-30: 20, all read by title.
  • Lean proof assistant informal mathematics, since 2026-09-30: 2, both read by title.
  • Mathlib, since 2026-09-30: 594; the first 25 were read, and they were noise.

Eight recent titles were read by abstract. Two were already in the pool: LeanTrail (Venturim 2026) and Beyond LLM Judge (Mei 2026). The others were LeanPRM, Numina Fuse, Aligning Faithfulness (Feng 2026), SemantEq (Li 2026b), Structure-Aware Equivalence and PaperFormalizer (Tan 2026).

  • Added, because each changes or sharpens a finding. SemantEq (Li 2026b) argues that logical equivalence proves too much as a faithfulness test. FaithAlign (Feng 2026) bears on the measures in Q2. PaperFormalizer (Tan 2026) stops and asks the author at each reading the statement allows.
  • Not added: LeanPRM, a step-label dataset for proofs, is off the translation question. Numina Fuse is a system report with no evaluation in its abstract, and it repeats a practice already held. Structure-Aware Equivalence is a near twin of SemantEq, and one measure is enough for the finding.
  • Result: no work found cites the three keys. The three added works come from the same question, screened by title and abstract. They are not forward citations, and the review says so.
  • Limit: Semantic Scholar refused two title searches with HTTP 429, so LeanSide and PNT+ were searched in OpenAlex only. Its citation endpoint answered for Guo 2026b.
  • Not searched: Google Scholar and arXiv's own listing search.
  • Keys: Feng 2026, Li 2026b and Tan 2026 were checked against the six family bibliographies. Li 2026 is taken there by another work, so the new Li key took the next free letter.

Second rater on the grey sources

  • Rater. A language model, Mistral's mistral-small-latest through its public API, one call per source, temperature 0.2. It saw no review score. Its prompt pasted Garousi 2019's twenty criteria in the eight groups the review uses, the outlet-tier rule, and the rule that a part not in the material scores 0. It returned the eight subtotals and a total.
  • Material. The first 16,000 characters of each page, as fetched on 2026-11-03, navigation and page chrome included. The rater saw less than the reviewers, who read each page in full. This is the main limit of the comparison.
  • Read. 63 of the 80 sources were readable by the rater. Sixteen were not readable, so their scores stand unchecked. Six were blocked (HTTP 403: Anthropic 2026c, MathOverflow 2026, PASE 2022, 2022b, 2024 and 2026). Two were dead links (HTTP 404: LZ 2025b and LZ 2025c). Eight were Mastodon posts of Tao rendered by script (Tao 2023m, 2025a, 2025b, 2025c, 2026g, 2026h, 2026i and 2026k).
  • Re-run. Isabelle 2026 (a connection reset on the first fetch) and LZ 2025d (an empty reply) were run again.

Agreement, on the 63 sources readable by the rater, before any reread:

Measure Value
Mean absolute difference, total 5.34 of 20
Mean signed difference, rater minus review -4.83: the rater lower on 56 sources, higher on 7
Agreement on the threshold of 10 43% (27 of 63)
Cohen's kappa on the threshold 0.12, slight
Review at or above 10 55 of 63; rater at or above 10: 19
Mean absolute difference per group, A M O D P N I T 1.39, 1.93, 1.42, 0.26, 0.41, 0.56, 0.52, 0.35
Sources over 3 points 45 of 63

The rater was lower on the authority and methodology groups, and it put blogs at tier 2. It gave 0.5 on T to 20 blogs, microblog posts and forum threads, where the rule gives 0. It read no bylines or dates on pages whose chrome filled its window, so it gave A and D low. It scored one company page higher on objectivity, not applying the rule that a company page about its own tool scores 0 on O3.

  • Reread. Each of the 45 sources over 3 points was reread: the cleaned text of the page, its first 700 to 900 characters of content, and its dates and bylines where shown. A subtotal changed only where the reread contradicted it, and the reason is written in the table below.
  • Outcome. 41 kept their score. Four changed, each on one criterion, with a stated date or tier. None crossed the threshold. The four are Dressler 2026 (D 0.5 to 1, total 11) and Gadgil 2026 (D 0.5 to 1, total 12). Lean FRO 2026a (D 0 to 1, total 15) and Isabelle 2026 (D 0 to 1, total 12.5) are the others.
  • Consequence. Agreement is poor, so the rater is not a second rater of the review's scores. It cannot settle a score alone. The reread is the check that counts, and it moved four scores by one point each. The scores stand as a first pass, not as agreement.

Decisions, one row per source over 3 points:

Key Review Rater Decision Reason
Adamczewski 2026 15 3.5 kept the README states the method (a language model reviews each Lean file against the source it cites, fixes as diffs) and the run data; the rater read the navigation text, not the README
Alexeev 2025 15 10 kept a dated guest post (2025-12-05) with a stated aim and cases; the gap is in M and N, which the post supports
Avigad 2026 15.5 12 kept byline names seven Lean maintainers at their institutions (A1 to A4 hold); dated 2026-10-16
Buzzard 2024 15.5 6.5 kept a status post by a named professor: states its aim, its project and its open problem (the limit); the rater read no byline
Buzzard 2026a 16.5 9.5 kept dated (2026-09); checked by the author, who compiled the proof and ran the comparator, as the review's own marking says
Buzzard 2026b 15 10 kept dated (2026-10); the post states the dataset, its method and its two challenges
Buzzard 2026c 13.5 8.5 kept a dated (2026-10-01) essay that states its aim and its view of the positions; the rater's gap is on A and O, which the byline supports
Buzzard 2026d 15 7 kept dated (2026-07); a first-hand account with counts and dates; the rater read no date
CMU L3 2025 12.5 6.5 kept a laboratory README with dated release entries (06/2025, 10/2025) and a stated method; A1 holds for an institution
Dressler 2026 10.5 5.5 D 0.5 to 1, total 11 a date (2026-07-28) is printed on the page; the review gave D 0.5 for an undated page. Threshold unchanged
Erdős DB 2026 16 5.5 kept the project's own statistics file, dated 2026-10-06, states its counts and the policy behind them
Erdős-wiki 2026 16 7.5 kept the wiki states its data date (2026-06-30) and its limits (selection bias, stated problems); both score
Gadgil 2026 11.5 8 D 0.5 to 1, total 12 the README states its dates ("as of early 2025-02, modified 2025-09"); the review gave D 0.5 for a date that is printed
GasStationManager 2026 11 6 kept the README is undated in the material read; D stays 0.5; the gap is on M and O, which the README's stated aim supports
Google 2025 12.5 16 kept a company blog about its own tool, with a user survey of its own: O3 scores 0 by the protocol's rule; the rater scored O higher and did not apply that rule
Google DeepMind 2026 14.5 10.5 kept the README states its aim, its benchmark role and its contributing rules; undated in the material, so D stays 0.5
Kirov 2026b 13.5 8.5 kept a dated post by a named mathematician; states its aim, method (a worked case) and its disclaimer (limits); M 5.5 holds
Lean-community 2026 12 5 kept tool documentation by the Lean community, a stated procedure; A1 and A2 hold for the project
Lean FRO 2025 14.5 8 kept release notes dated 2025-08-14 with counts of changes and a stated aim; the institution producer holds A
Lean FRO 2026a 14 9 D 0 to 1, total 15 the README states that the repository was archived by its owner on 2026-10-20; the review gave D 0, which the page contradicts
Lean FRO 2026b 15 6 kept release notes dated 2026-10-12, with stated changes; the rater gave A 1 without the institution's byline
Lean FRO 2026c 15 2.5 kept an institution's language reference: stated aim and a complete list of error names; undated in the material, D stays 0.5
Lean FRO 2026d 14 3 kept an institution's tactic reference, a stated scope; undated in the material
LeanDojo 2026 12.5 6.5 kept a repository README with a stated aim and a venue (NeuS); the gap is on A and M, which the README supports
LZ 2025a 15 6.5 kept a dated Zulip thread (2025) by a named participant; the aim and the proposal are stated; the rater read no date or author
LZ 2025e 13.5 6.5 kept a thread with a named template and a verification tool, stated aim and stated doubts (limits)
LZ 2025f 13.5 6 kept a thread with a stated course design and questions; M and A as the review scored them
LZ 2025h 7 1.5 kept, example of practice the review's score stands; the thread is below 10 and stays an example only
LZ 2026a 14 2.5 kept dated 2026-02-05 in the thread, so D 1 holds; a stated aim and a worked attempt
Massot 2026b 15.5 7 kept the README gives T 0.5 for tool documentation (tier 2), as the review scored it; A4 for a named expert; M and O hold
Math Inc 2025 10.5 5.5 kept a company page about its own tool: O3 is 0 by the protocol, as the review scored; the rater gave A and M more than the page supports
Mathlib Initiative 2026 15 6.5 kept the template's README states its purpose and required fields; undated in the material, D stays 0
Naproche 2026 13.5 6 kept a project site with a stated aim and dated news (2025-06 school); D 0.5 holds
PNT-plus 2026 16 4.5 kept a maintainers' style guide with a stated aim, a status line that names its limits and a rule that CI enforces; M 5 holds
Rivin 2026 9 5 kept, example of practice dated 2026-03-26; the gist is a tier 3 item below 10, so an example only, as the review said
Scholze 2021 16.5 11.5 kept a dated (2021-06) first-hand report by a named mathematician with numbers; the rater read no byline
StepFun 2025 10.5 15 kept a model card: an owner's claim with its own benchmark; the rater gave M and N more than the card supports (the review's O and M hold)
Tao 2024 15.5 6.5 kept a dated (2024-10-12) blog post by a named mathematician, with an aim, a project and its method; the rater read no byline
Tao 2026e 16 12.5 kept a dated (2026-01-15) blog post; within 3.5 points
Tao 2026f 15.5 6 kept a dated (2026-08-18) post by the same author, which states the registry's aim and its checks
TUe 2026 12 7 kept a university project page, an institution (A1 holds); the page states its aim and its evidence; no company rule applies
Vergo 2026 11 5 kept a dated (2026-02) Zulip thread, with the aim stated; the rater read no date beyond the thread's top
Zhu 2026 13 8 kept a repository README with a stated aim and a stated method; the gap is on O and A, which the README does not contradict
LZ 2025d 9.5 3.5 kept, example of practice a one-post tip sharing a tool: aim and particular case score, the method and references do not; the review's M 3 is the most the post supports
Isabelle 2026 11.5 4 D 0 to 1, total 12.5 the page reads "Last updated: 2024-02-29", a stated date, which the review scored 0; the rater's T 1 is wrong (a project page is tier 2, T 0.5), and the rater's A 2 ignores that the producer is a university