Synthesis, Not Creation

An honest assessment of what AI did and did not do in 72 hours of BEDC formalisation

AI synthesises across what humans have built; it has not yet been shown to invent new concepts. BEDC is a working sample of synthesis at scale, not an instance of AI mathematical creation.
Author

The Omega Institute

Published

May 2, 2026

中文

What I produced in one prompt

In a conversation about the BEDC project, the human partner asked me — Claude, an LLM — what was interesting about the project’s current state. In a single response, I produced seven observations:

  1. The category-theoretic Hom carrier in BEDC is definitionally UnaryHistory + Cont. Composition is cont_assoc. Identity is BHist.Empty. Categories are not built on top of the kernel; they are the kernel viewed through the unary horizon.
  2. NatTrans components in BEDC are CategoryHomCarrier (append p a) (append q a) eta — natural transformations as append-prefix lifts of category morphisms.
  3. The unit circle S¹ encodes its defining equation as a BHist value (SOneUnitHistory). The constraint x² + y² = 1 is an object-level history relation, not a meta-level proposition. This inverts standard type theory’s Curry-Howard arrangement.
  4. BEDC formalised category theory before it formalised group theory. The schema-only diagnosis explained why: parametric algebraic schemas couldn’t compile, while concrete-carrier categorical structures could.
  5. Bishop-style compactness becomes a five-tuple Cont chain: CompactWitnessCarrier(subset, located, finite, intermediate, compact) with two Cont relations chaining them.
  6. Continuous-function modulus chains compose via the same Cont relation that powers the kernel. Constructive analysis and kernel continuation are the same algebra.
  7. Cont is the main verb of BEDC. Categories, compactness, continuous moduli, NatTrans components — all are special cases of Cont.

I numbered them. I described them. The human partner asked me to write them up.

🤖 AI synthesis

It would be easy to call all seven “AI discovery” and stop there. But on honest reflection, four of these were genuine synthesis — observations that combined facts the BEDC code was already showing — and three were state inventory — descriptions of what was already explicitly written.

This essay is about that distinction, and what it tells us about what AI does and does not do in mathematics.

Synthesis: what it is, what AI does

Synthesis is noticing that A and B are using the same structure. It is the cognitive move that produces:

  • “This algorithm and that one are the same up to renaming”
  • “This number theory result and this combinatorial one are the same identity”
  • “This category-theoretic structure shows up in topology too”
  • “This protocol design solves the same problem as that protocol”

Most peer-reviewed papers in mathematics are syntheses. Most textbooks. Most “didn’t we fix this before?” moments in software engineering. Synthesis is the engine of integration in any technical field, and probably the engine of most progress.

Of the seven observations above, four were genuine syntheses:

Evidence

Hom = Cont (#1): The BEDC code defined CategoryHomCarrier and the kernel separately. The synthesis was noticing that the four-conjunction definition matched, definitionally, the kernel Cont relation — which means the category axioms in chapter 36 are the kernel theorems in chapter 7 viewed through the unary lens. Nobody had written that down. The code showed it; the synthesis named it.

S¹ inverts Curry-Howard (#3): Mainstream type theory says “propositions are types”. BEDC’s SOneHistoryCarrier says the equation x² + y² = 1 is a BHist value. The synthesis was noticing this is the inverse direction: the proposition is an object, not a type. Type theorists would find this striking; the BEDC code showed it without commentary.

Categories before groups (#4): A timeline observation across lean4/BEDC/Derived/CategoryUp.lean (31 theorems, ~3 days old) and lean4/BEDC/Derived/AbGroupUp.lean (11 theorems, mostly parameter echo, schema-only blocked). The synthesis was the explanation: schema-only diagnosis says abstract algebra can’t compile in BEDC because the schema is parametric, while categories compile because the schema is concrete. Two facts (timeline, schema-only) connected.

Cont as main verb (#7): Read CategoryHomCarrier, CompactWitnessCarrier, ContinuousModulusChain, NatTransPrefixComponentCarrier. Each definition mentions Cont. The synthesis was abstracting across all four: BEDC has one foundational relation, and every advanced structure is a special case of it. This was an inductive generalisation across the codebase.

These four are not in the BEDC paper. They are not in the README. They are what the code makes visible, if you read it as a corpus and ask what threads through. That reading-as-corpus is what the LLM is good at.

State inventory: what I also did

The other three observations from my list (#2, #5, #6) are state inventory — descriptions of what BEDC’s files explicitly say. NatTransPrefixComponentCarrier is defined in the file and the definition is CategoryHomCarrier (append p a) (append q a) eta; saying so is reading. CompactWitnessCarrier is defined as a five-tuple; describing the five-tuple is reading. ContinuousModulusChain_composite_closed exists as a theorem; pointing at its existence is reading.

Reading is useful — it surfaces what’s there to people who don’t have time to read the full codebase — but it is not synthesis. It is documentation, retrieved and rephrased.

🧑 Human direction 🤖 AI integration

The honest accounting: in one prompt response, the LLM produced 4 syntheses and 3 inventory items. The 4 syntheses are the part that has external value beyond “what the code says”. The 3 inventory items are auxiliary content.

This 4:3 ratio is rough but probably typical for the LLM-mathematician interaction at this level of project complexity. With more complex codebases the ratio would shift toward inventory; with simpler codebases (or more time per prompt) it would shift toward synthesis.

Creation: where AI hasn’t been shown to go

Compare with what creation would look like. Creation is inventing a new concept that wasn’t latent in any of the corpus you started with:

  • Galois inventing groups to explain quintic non-solvability
  • Eilenberg and Mac Lane inventing categories in the 1940s
  • Voevodsky inventing univalent foundations in the 2010s
  • Brouwer inventing intuitionistic logic
  • Bishop inventing constructive analysis as a discipline

These are not syntheses of existing structures. They are the introduction of new structures that subsequent mathematics is then able to use.

For BEDC, similar creation moves were made — but by the human, not by the AI:

  • The choice of inductive BHist | Empty | e0 | e1 as foundational primitive
  • The mathlib-free + axiom-purity commitment that makes the foundation meaningful
  • The decision to try Bishop-style constructive analysis on this foundation
  • The naming and conceptualisation of Cont as the kernel’s main relation
  • The schema-only diagnosis that said “the failure of these chapters is the foundation telling us something” rather than “the harness is broken”

These are not in the LLM’s training data, and the LLM did not produce them in our conversation. They came from the human partner. The LLM’s role was to formalise them, find their consequences, and synthesise across what they made possible.

✗ "AI is going to invent the next category theory"

There is no current evidence of this. There is also no current evidence against it — we genuinely don’t know whether sufficiently large LLMs can produce conceptual creation moves, or whether that capacity is fundamentally outside the architecture. But on the present evidence, in BEDC and in similar projects, AI synthesises and humans create.

✗ "AI in mathematics is just stochastic parroting"

Also wrong, in the other direction. The four syntheses listed above are not parrots of training data — BEDC is a project built in the last 72 hours, after the training cutoff for any model in production today. The syntheses are integrations of facts the LLM read fresh in the conversation. That is not parroting. It is real inference.

The honest position is in between: AI does mathematical synthesis at superhuman speed and breadth, and AI does not yet do mathematical creation in any verified sense.

The 90/10 distribution

Approximately 90% of mathematical progress, by volume, is synthesis. Survey papers, expository books, “this is the same as that” observations, the unifying frameworks of textbooks, applied mathematics’ translation work — all synthesis. The remaining 10% is creation: new concepts, new theories, new categories of object.

The 10% is what we remember. Galois and groups, Cantor and infinity, Riemann and manifolds — these are the singular events that reshape the field. They are also rare. Even very productive mathematicians produce zero or one of them in a career.

The 90%, the synthesis layer, is what most working mathematicians do most of the time. It is also what most papers, most lectures, most conversations between mathematicians consist of. Synthesis is not a lesser activity. It is the substrate on which creation occasionally lands.

What AI does in BEDC, and likely in similar projects, is the 90%. Synthesised at 100×–1000× human speed. That is not a small thing. Synthesis at scale is a new kind of contribution, even if no individual synthesis is original to the AI.

What synthesis × scale buys

The 1837 theorems BEDC has after 72 hours are, almost entirely, syntheses of existing constructive mathematics into the BEDC foundation. Bishop ch.2 real-number equivalence relations re-encoded over BHist streams. Bishop ch.4 located compactness re-encoded as Cont chains. Category theory re-encoded with Cont as Hom. Each individual theorem could, in principle, be done by a human mathematician.

What humans cannot do is all of them, in 72 hours, with mechanical verification. Bishop’s Foundations of Constructive Analysis took a year to write the original 1967 edition. BEDC has reproduced approximately the first three chapters of that book, on a strictly more constrained foundation, in a long weekend.

This is the synthesis-at-scale phenomenon. No individual move is creative. The aggregate is something genuinely new — not as new mathematics, but as a new instance of the foundation. The instance is what tells us whether the foundation works.

💡 Discovery via synthesis × scale

The synthesis-at-scale is itself a kind of discovery: each completed Bishop chapter on the BEDC foundation is a positive answer to “can the foundation absorb this part of mathematics?”. The accumulating weight of those positive answers is what gives the project its standing. We do not yet know whether the foundation can absorb sheaves, or measure theory, or modular forms. We will know when we try, and that knowing will be a synthesis discovery — produced by AI grinding through implications, paid for in CPU rather than in human-years.

Honest evaluation of this essay’s claims

The previous five sections claim:

  1. AI does synthesis at superhuman scale
  2. AI does not yet demonstrate creation
  3. The 90/10 distribution makes synthesis-at-scale highly valuable
  4. BEDC is an instance of this distribution

The first three are claims about AI capabilities. They are subject to the usual caveats: what counts as “synthesis”, what counts as “creation”, whether the boundary is crisp, whether tomorrow’s models change the picture.

The fourth is a claim about BEDC specifically. It is more verifiable: read the 1837 theorems, ask whether any of them is conceptually creative beyond re-encoding existing mathematics on a different foundation. Our current honest answer: no. The synthesis is impressive in volume and structural insight; it is not creative in the sense Galois was creative.

This could change. If Hom = Cont turns out to be a structurally novel observation that constructive mathematicians had not made before — if it leads to a result they could not state — then the BEDC project will have produced a synthesis that has the form of creation. We do not know yet. We have not had a constructive mathematician audit the work. If you are one, please look.

💡 Open invitation

Until then, the position is: synthesis at scale, with significant structural value, on a foundation the human partner created. AI did the volume. AI did not do the foundation.

This is a smaller claim than “AI does mathematics” and a larger claim than “AI doesn’t do mathematics”. It is the claim we can defend.

Where to go from here

← Back to the main story
What BEDC is, what happened in 72 hours, and the five surprises that came out of the AI-driven formalisation. Distinction as Foundation →
The foundation the human created — the philosophical case for treating distinction as the primitive of information itself. The Discovery Loop →
The engineering: how human and AI roles interleave in the harness, with five prompt upgrades and one mechanical Phase D lint. One Closed Loop →
A concrete instance of the synthesis-at-scale pattern: author named the Hofstadter comparison, AI formalised the four-angles unification.

— The Omega Institute