# AI provenance: BLLM: Beyond the LLM with Deep Human-Mind-AI

Authors: Deep Bhattacharjee (corresponding author, ORCID 0000-0003-0466-750X;
formerly EGSPL, Bhubaneswar, Odisha 751030, India, and formerly University of
Calcutta, Senate House, 87/1 College Street, Kolkata 700073, West Bengal,
India) and Ushashi Bhattacharya (ORCID 0009-0002-2254-3914; formerly National
Taiwan University, Taipei 106319, Taiwan).

- Paper: https://github.com/creelie/eBLLM/blob/main/preprintBLLM/BLLM.pdf
- Package eBLLM and engine Anaxia, with the paper's source, Lean
  formalisation and checks in `paper/bllm`: https://github.com/creelie/eBLLM,
  release v3.0.0, Zenodo https://doi.org/10.5281/zenodo.23464390 (all versions
  https://doi.org/10.5281/zenodo.23286641)
- Container image of the engine: ghcr.io/creelie/bllm-engine (no model
  weights)

## Result

Inside a model of randomized checks the paper computes the least cost of
soundness:

- the entropy law (Theorem A) and its exact optimum through Kraft vectors and
  Huffman codes (Theorem B);
- the Rényi law for checks of polynomial order (Theorem C);
- the singularity criterion Σ a_n log(1/a_n) < ∞ (Theorem D);
- the branching takeoff (Theorem E), the chain law (Theorem F) and
  step-versus-outcome gating (Theorem VIII.2);
- the online law (Theorem G), subagents (Theorem H) and cascades
  (Theorem XI.1);
- the gap law (Theorem I): a proposer needs at least e^{H_{1/2}(π)}
  proposals, attained only by square-root sampling, and language models need
  1.5 to 4.3 times this;
- the tower law (Theorem XIV.1): n verified layers sharing one budget θ of
  false acceptances cost at least n log(n/θ), each added layer at least
  log((n+1)/θ) more, and past a finite depth every tower costs more than any
  fixed amount.

It then measures Anaxia, an engine built on these laws, on five open
problems (the Yang–Mills mass gap, the Hodge conjecture, the standard
conjecture of Lefschetz type, Chowla's conjecture and Erdős problem 1183):

- Typed crossing reached in every run a composite accepting a lattice mass
  gap for four-dimensional SU(2) on β_W < 1/3, which no random or
  type-filtered run reached. The composite was first proposed by the language
  model, so the network reproduces the step. The step, m ≥ −log(3β_W), is
  proved in the paper (Theorem XVII.4) and has not been refereed; no forest
  gauge fixing goes past 1/3 (Proposition XVII.5).
- Hebbian boosters add nothing; shared memory reaches the same plateau with
  about half the checks; five agents reach it sooner and no further; of 38
  transfers of a barrier-breaking pattern none closes.
- Construction mode rebuilds, from the rules of Steinberg's problem alone,
  the 15-vertex and 42-vertex gadgets of the 2016 counterexample of
  Cohen-Addad, Hebdige, Kráľ, Li and Salgado and the 166-vertex
  counterexample itself. These are rediscoveries of a published construction.
- At equal budgets of exact checks (120 runs), a second layer of builders
  whose curriculum turns an easier gadget into a lemma reaches the second
  gadget on 7 of 10 runs where the builder alone never does; a third layer
  adds nothing; random crossing finds no gadget at 13 to 20 times the budget;
  nothing is found on Erdős's question for cycles of length 4 to 6.
- Twelve rounds on the Hodge conjecture alone leave the gap of every target
  point where it was; counting excludes two configurations on E_0^6 and
  reduces two others to explicit Massey products. (F2) and (F3′) remain open.
- In Erdős problem 1183 a reduction of level colourings to weighted posets
  (Lemma XVII.1) gives the upper bounds that, with the known lower bounds,
  determine f(n) for n ≤ 20 (Theorem XVII.2), with f(20) = 12. The lower
  bound for odd n ≥ 11 is the OpenRefute Lean theorem, and f(20) ≥ 12 is
  Theorem 7.6 of the fifth version of Bhattacharjee, Mandal and Bhattacharya
  (https://doi.org/10.5281/zenodo.23374973), whose proof ends in a finite
  check; both are credited.

## Who did what

Deep Bhattacharjee chose the problems, directed the work, set the format and
ran the computations. Claude (Anthropic), used through Claude Code under his
direction, produced the proofs, the Lean 4 formalisation, the engine and its
benchmarks, the checking programs in Python, C, C++, Julia and shell, the
figures, the LaTeX text and its reference list (every reference was checked
against the publisher's, Crossref's, zbMATH's or the archive's record), and
this file. No other AI system took part, apart from the language models
measured as proposers in the experiments. Claude is not listed as a
contributor.

## How the result is checked

- Lean 4 with Mathlib: sixty-five theorems covering every finite inequality
  of the model and the tower law (Appendix B), each depending only on
  propext, Classical.choice and Quot.sound; no sorry, native_decide or added
  axiom.
- Independent Python, C and C++ programs: 55,271 checks, no failure.
- Every gadget of construction mode passes a gate (planarity with the
  contacts on one face, the forbidden cycle lengths, the contact distances,
  and the forced colouring by a satisfiability solver) that shares no code
  with the search; the 166-vertex graph is found not 3-colourable by three
  solvers.
- Erdős 1183: each colouring for n ≤ 10 checked by an exact search and by a
  satisfiability query that shares no code with it; 11 ≤ n ≤ 19 by the
  exhaustive weighted-poset search, with n = 11 confirmed also by the exact
  search over all sublattices and by a satisfiability query; n = 20 by the
  poset search, which finds 59 level colourings with no monochromatic
  sublattice of 13 members.
- Every measured number of the experiments and of the tower bench is
  produced by the eBLLM 3.0.0 package from fixed seeds; the logs and raw rows
  are archived with it.

## What is not claimed

The paper does not claim that Anaxia or any BLLM proves the Hodge
conjecture, the Yang–Mills mass gap (the Clay problem) or any of the five
problems; none is solved. Construction mode rediscovers a published
construction and does not claim a new theorem on Steinberg's problem. The
tower bench is small (three targets, five seeds, depth up to three). It does
not claim f(n) = O(n). The β_W < 1/3 theorem is a lattice result at strong
coupling, not the continuum mass gap. The probabilistic limit theorems are
proved or cited in the text and are not formalised.