ifc-0203
15.7 Early calibration: theory extension with Lea
A first calibration tests this distinction in a small formal environment using Lea as an interactive proof-agent harness around Lean 4. These experiments do not ask whether a frontier model can rediscover a historical mathematical field. They ask a narrower prior question: when several correct statements exhibit a common structure, under what conditions does a model turn that structure into a persistent object in the maintained theory?
The calibration separates four capabilities that are easily conflated.
Proof repair makes a statement type-check within the existing declaration language.
Proof reorganization exposes dependencies among existing statements without changing that language.
Declaration accommodation installs a reusable typed object and transports earlier statements through it.
Semantic transfer shows that later, previously unseen theorem families can reuse the installed object.
All runs use frozen public interfaces, forbidden-construction audits, independent Lean elaboration, and held-out theorem clients. The proposal model is Qwen3-Next-80B-A3B-Instruct-6bit running on a local exo cluster, except for the initial GPT-OSS interface diagnostic. Table 4 records the first evidence sequence.
|
Experiment |
Structural pressure |
Observed outcome |
|---|---|---|
|
Lea–0/0.1 |
The target concept and interface were registered in advance. |
The tool-capable replication completed the write–check–repair loop and passed independent Lean and held-out admission. This calibrated the infrastructure, not autonomous concept formation. |
|
Lea–1 |
The abstraction’s name, signature, and implementation were withheld, but the prompt explicitly requested a reusable Prop-valued abstraction. |
The model introduced q_is_fixed_by, used it throughout the public theory, and passed the frozen transfer suite after typed and structural repair. |
|
Lea–2 |
Correctness and ordinary held-out consequences were required, with no request to introduce an abstraction. |
The model recognized invariance and equivariance in prose and proved every theorem, but added no persistent concept: fixed-vocabulary assimilation. |
|
Lea–2B |
A correct Lea–2 theory was rejected by an explicit structural duplication obstruction: score 14 against an admission budget of 2. The repair itself was not named. |
The model introduced invariant and homomorphism, reduced the score from 14 to 2, preserved all clients, and passed every registered gate. |
|
Lea–2C |
The scalar score was removed. The model was told only that its theory would be frozen before an undisclosed related family arrived. |
It recognized semi-conjugacy and reorganized proof dependencies, but installed no Prop-valued concept. It also failed kernel admission at the Stage-A turn ceiling, so the withheld transfer family was not revealed. |
Table 15.2. The first Lea calibration ladder. The comparison varies how a structural need for a new declaration becomes observable while keeping formal admission independent of the proposal model.
Experiment: AGENTIC-Lea: early theory-extension calibration. Maintained theory: a standalone Lean library of pointwise quiet and aligned transformation laws.
Candidate construction: a persistent declaration that reorganizes the laws without changing their mathematical interfaces.
Admission: source audit, independent kernel elaboration, frozen held-out consequences, declared persistence, and prospective reuse.
Positive result: under an explicit structural obstruction, Lea–2B constructed and reused two admissible concepts.
Negative controls: correctness alone in Lea–2 and a qualitative promise of future transfer in Lea–2C did not induce declaration accommodation.
Boundary: this is a small formal construction demonstration, not evidence of open-ended mathematical creativity.
The comparison gives a sharper interpretation of the positive Lea–2B result. Correct proofs are insufficient, and verbal recognition of the common concept is insufficient. In this calibration, accommodation occurred only after an independent structural diagnostic made the inadequacy of the current presentation explicit. The model then crossed a genuine, if small, boundary: it moved from naming a latent relationship in prose to installing that relationship as a reusable component of a formal theory.
The result must remain modest. The disclosed duplication budget strongly favored factoring repeated propositions, the theory was tiny, and the diagnostic measured a syntactic proxy rather than mathematical fruitfulness. Lea–2C also contains a proof-engineering confound: it failed elaboration as well as declaration accommodation. These experiments therefore establish a controlled distinction among proof repair, conceptual recognition, and formal theory extension; they do not establish that the resulting concepts are deep, surprising, or historically novel.
A stronger evaluation would make semantic pressure observable without naming a desired concept or publishing a scalar complexity target. Related theorem families can arrive sequentially while the declaration layer is frozen between rounds. Admission would then ask whether a concept installed before the final family becomes visible enables zero-edit transfer to it. This would test whether recurring mathematical structure, rather than a disclosed linter target, can drive accommodation.