% written by figures/src/make_sources_table.py from src/ebllm/bllm/data/sources.json
\par\begingroup\footnotesize\raggedright\setlength{\parindent}{0pt}\setlength{\parskip}{2pt plus 1pt}%
\def\sourcegroup#1{\par\addvspace{4pt}\textbf{#1}\par\nobreak}%
\def\sourceentry#1#2#3#4{\par\hangindent=1em\hangafter=1 \textbf{#1}, #2. \emph{Takes:} #3 \emph{Leaves:} #4\par}%
\sourcegroup{Google DeepMind}
\sourceentry{FunSearch \cite{RBN24}}{refereed}{Evolve and evaluate: a population of strategies, each scored by an exact evaluator; the better ones are kept and mutated. \emph{In:} src/ebllm/construct/tower.py (Layer2); the funsearch constructions are indexed by src/ebllm/bllm/deepmind.py.}{Program mutation by a language model and the island model: no model runs in construction mode.}
\sourceentry{AlphaEvolve \cite{NVE25}}{preprint}{The evaluation cascade: cheap tests discard most candidates before the expensive test, and the evaluator, not the proposer, decides. \emph{In:} src/ebllm/construct/proof\_builder.py (try\_add: forbidden cycles, contact distances, planarity, then the SAT forcing check, then minimise) and tower.meets (the gate).}{The Gemini ensemble and the evolution of whole programs; the 67 construction problems and AlphaEvolve's results enter only as indexed targets and library nodes.}
\sourceentry{AlphaProof \cite{HMS25}}{refereed}{A curriculum: easier variants of the target are solved first and what they yield is kept for the target. \emph{In:} src/ebllm/construct/tower.py (Layer2.profile: the target's weaker contact profiles first; each gadget found joins the library as a lemma).}{Reinforcement learning, the formaliser network and the Lean proof search; the AlphaProof Nexus proofs are read by src/ebllm/bllm/corpus.py (read\_alphaproof).}
\sourceentry{AlphaGeometry \cite{TWL24}}{refereed}{Deduction run to a fixed point, with a construction proposed only when deduction stalls. \emph{In:} src/ebllm/construct/proof\_builder.py (status: the shared colour spreads by forward rules; Builder.moves: attach, link and lemma moves when no closing move applies).}{The language model that proposes auxiliary points, and the geometry engine DDAR itself.}
\sourceentry{AlphaGeometry2 \cite{CTO25}}{preprint}{Nothing beyond AlphaGeometry's division of labour; pinned and fetchable. \emph{In:} anaxia fetch deepmind alphageometry2.}{DDAR2 (geometry only).}
\sourceentry{Formal Conjectures \cite{FCA25}}{software}{The statements with their open or solved status: the target catalogue and the check that a target is still open. \emph{In:} src/ebllm/bllm/deepmind.py (index, Search); anaxia intake deepmind -{}-search.}{The Lean statements are not compiled by Anaxia.}
\sourceentry{Mathematics dataset \cite{SGH19}}{refereed}{Pinned as a generator of warm-up questions for a local proposer. \emph{In:} anaxia fetch deepmind mathematics\_dataset; experiments/ fine-tuning script.}{Not used in any construction-mode run or measurement.}
\sourceentry{AlphaTensor \cite{FBH22}}{refereed}{The decompositions, indexed as library constructions. \emph{In:} src/ebllm/bllm/deepmind.py.}{The reinforcement-learning game.}
\sourceentry{AlphaDev \cite{MMZ23}}{refereed}{The sorting programs, indexed. \emph{In:} src/ebllm/bllm/deepmind.py.}{The method.}
\sourceentry{Mathematics conjectures (Davies et al.) \cite{DVB21}}{refereed}{The notebooks, indexed. \emph{In:} src/ebllm/bllm/deepmind.py.}{The attribution method, which needs data of a kind the targets do not supply.}
\sourceentry{Aletheia and LEAP (superhuman), \nolinkurl{github.com/google-deepmind/superhuman}}{software; outputs unrefereed}{The generate, verify and revise loop with a verifier independent of the generator, which is the refuter pass; one Aletheia output as a library node of the Hodge attack. \emph{In:} src/ebllm/bllm/superbrain.py and hodge.py (the refuter pass); experiments/hodge/absorb\_sources.py.}{The Erd\H{o}s, Kirby and FirstProof outputs.}
\sourcegroup{Methods}
\sourceentry{Successive halving \cite{JT16}}{refereed}{Keep the better half of the arms after each round. \emph{In:} src/ebllm/construct/tower.py (LayerK).}{-{}--}
\sourceentry{Hebbian learning \cite{Heb49}}{book}{A connection used in a success is strengthened and every connection decays. \emph{In:} src/ebllm/construct/tower.py (Mesh.reinforce, Mesh.bias).}{-{}--}
\sourceentry{Postnikov towers \cite{Hat02}}{book}{The framing of the layer tower: stage n is the engine cut at depth n and each stage is the one below with one layer added; an analogy, not a construction of a Postnikov tower. \emph{In:} paper; Lean BLLM.tower\_increment states the precise part (each added layer raises the cost bound).}{-{}--}
\sourcegroup{OpenAI}
\sourceentry{OpenAI mathematics manuscript collection \cite{OAI26b}}{unrefereed claims (the collection says that some unformalised results could have issues)}{The move statistics of the crossing network and an index of the manuscripts for the check that a target is still open, every item marked unrefereed. \emph{In:} src/ebllm/bllm/corpus.py (read\_openai); src/ebllm/bllm/sources.py (index\_openai).}{The claims themselves.}
\sourceentry{OpenAI Navier-Stokes Lean proof \cite{OAI26}}{Lean build checked; paper unrefereed}{A literature row with its status; its build record applies the rule of Anaxia's Lean check (kernel check, only propext, Classical.choice and Quot.sound). \emph{In:} src/ebllm/bllm/sources.py (registry).}{Nothing of the mathematics enters the engine.}
\sourcegroup{The Omega Institute}
\sourceentry{trureturing (OpenRefute) \cite{OIT26}}{Lean results kernel-checked; the reading of each paper's statement as a Lean claim is the repository's own and unrefereed}{An index of the 782 problem dossiers (statement, resolution, Lean declaration, link): refuter data, since it records which published conjectures fell to an explicit instance, and a source for the check that a target is still open. \emph{In:} src/ebllm/bllm/sources.py (index\_openrefute); anaxia sources check.}{The Lean library (not compiled here) and the judging tools.}
\sourcegroup{Memory}
\sourceentry{obsidian-brain \cite{Wei26}}{software}{Memory as a vault of linked notes, and retrieval that returns each hit with its link neighbours. \emph{In:} src/ebllm/bllm/vault.py (Vault.write; Vault.search: TF-IDF over the notes plus the notes a hit was built from or that were built from it).}{The Node server, the embedding model and the community detection.}
\sourceentry{claude-obsidian (lab009dm)}{software}{Notes captured with their provenance and linked to what they were built from. \emph{In:} src/ebllm/bllm/vault.py.}{The plugin and its health checks.}
\sourceentry{RealMythos, \nolinkurl{github.com/tszdanger/RealMythos}}{software}{Nothing: its content is vulnerability analysis; its staged layout (data, model, environment, traces) is already the layout of Anaxia's benchmark.}{All of it, as off-topic.}
\sourceentry{Advanced Reasoning MCP, \nolinkurl{github.com/creelie/advanced-reasoning-mcp}}{software}{The TF-IDF ranking of its memory search. \emph{In:} src/ebllm/bllm/deepmind.py (Search).}{The sequential-thinking tool with self-reported confidence.}
\sourcegroup{Agents}
\sourceentry{ultra-mathematician, \nolinkurl{github.com/txmy/ultra-mathematician}}{software}{The closure policy: closed only after a kernel-checked Lean endpoint with an audited statement and allowed axioms, never native\_decide; evidence levels lead, candidate, reproduced, formally verified, accepted. \emph{In:} the labels of anaxia controls and the release rule.}{The host-specific skills.}
\sourceentry{mathcode, \nolinkurl{github.com/math-ai-org/mathcode}}{software}{Only a strict check of one fully qualified declaration certifies completion, and stored assumptions are never injected silently. \emph{In:} the Lean verifier and the axiom audit (anaxia axioms).}{The CLI, web interface and backend.}
\sourceentry{open co-scientist (lab007dm)}{software}{Nothing in code: the tournament of hypotheses was considered and not built, since the checks and the refuter already rank survivors.}{The tournament and the research-agent stack.}
\sourcegroup{Corpora}
\sourceentry{OpenConjecture (lab010dm)}{conjectures as stated in arXiv papers; solver attempts unverified}{The candidate pool for conjecture attacks; six Hodge-related conjectures entered the Hodge library. \emph{In:} experiments/hodge/absorb\_sources.py.}{The model-reported solver attempts.}
\sourcegroup{Provers and models}
\sourceentry{DeepSeek-Prover-V2 \cite{RSX25}}{preprint}{Can serve as the proposer through an OpenAI-compatible server; its subgoal decomposition is the split of an obligation graph into steps. \emph{In:} src/ebllm/bllm/proposers.py (provider local).}{Not run in the paper's measurements (no GPU). Weights: not bundled; served by the user through the local connector.}
\sourceentry{Kimina-Prover \cite{WUL25}}{preprint}{Can serve as the proposer through the local connector. \emph{In:} src/ebllm/bllm/proposers.py (provider local).}{Not run in the paper's measurements. Weights: not bundled; served by the user through the local connector.}
\sourceentry{Goedel-Prover \cite{LTL25}}{preprint}{Can serve as the proposer through the local connector. \emph{In:} src/ebllm/bllm/proposers.py (provider local).}{Not run in the paper's measurements. Weights: not bundled; served by the user through the local connector.}
\sourceentry{Qwen2.5-Math \cite{YZH24}}{preprint}{Can serve as the proposer through the local connector; experiments/finetune/finetune.py fine-tunes a Qwen2.5 model (default Qwen/Qwen2.5-0.5B-Instruct) with LoRA on the choices the checks confirmed. \emph{In:} src/ebllm/bllm/proposers.py (provider local).}{Not run in the paper's measurements. Weights: not bundled; served by the user through the local connector.}
\sourceentry{Mathstral, \nolinkurl{mistral.ai/news/mathstral}}{model card}{Can serve as the proposer through the local connector or the mistral provider. \emph{In:} src/ebllm/bllm/proposers.py (providers local, mistral).}{Not run in the paper's measurements. Weights: not bundled; served by the user through the local connector.}
\sourceentry{HyperTree Proof Search (Meta AI) \cite{LLL22}}{refereed}{Search over an AND-OR tree of goals, which is the shape of Anaxia's obligation graph. \emph{In:} src/ebllm/obligations.py.}{The trained models. Weights: not released for Lean 4.}
\sourceentry{LeanDojo \cite{YSG23}}{refereed}{Premise retrieval: proposals are prompted with retrieved library nodes. \emph{In:} src/ebllm/bllm/memory.py (retrieval).}{The extraction tool and the trained retriever. Weights: not bundled.}
\sourceentry{Seed-Prover \cite{CGH25}}{preprint}{Lemma-style proving, in which proved lemmas are kept and reused: the same shape as the lemma library of construction mode. \emph{In:} src/ebllm/construct/tower.py (Library).}{The model (not released). Weights: not released.}
\sourceentry{Aristotle (Harmonic) \cite{ABB25}}{preprint}{Informal reasoning checked step by step in Lean, which is the contract of Anaxia's verifier.}{The system (not released). Weights: not released.}
\sourceentry{Language-model APIs}{services}{Proposers behind one interface; keys come from the environment. \emph{In:} src/ebllm/bllm/proposers.py.}{No key is stored in the package or the image. Weights: none: remote services.}
\par\endgroup