Durable experiment record · Local core code · frozen run records

AGENTIC-Lea theorem-construction ladder

Tool capability, scaffolded abstraction, fixed-vocabulary proof construction, structural repair, and early-stop tests.

21 code surfaces5 frozen runs2 code packagesic-lea

Experimental contract

What this family tests

developmental and controlled theorem-prover studies

The current catalog registers this at family and run level rather than assigning separate study titles.

Book-to-code crosswalk

The highlighted Experiment cards covered here

  1. Experiment: AGENTIC-Lea: early theory-extension calibration.15.7 Early calibration: theory extension with Lea · reported result or audit · direct family

Implementation map

From entry point to source surface

Start here

These concrete files are selected from the complete registered source surface to orient the reader.

  • runner · staged-not-public — synthetic-creativity-archive:agentic_lea_0/run_audit.pyLocate this file in the curated companion packet; no public download is currently offered.
  • external-dependency · public-pinned — lea-upstream:apps/lea-standalone/prover/examples/Ackermann.lean ↗Open the pinned public source file.
  • runner · staged-not-public — synthetic-creativity-archive:agentic_lea_0/run_lea.pyLocate this file in the curated companion packet; no public download is currently offered.
  • runner · staged-not-public — synthetic-creativity-archive:agentic_lea_1/run_audit.pyLocate this file in the curated companion packet; no public download is currently offered.

Author-declared entry points

  • packet scripts invoking Lea

Resolved code

external-dependency · 4
runner · 17
  • synthetic-creativity-archive:agentic_lea_0/extract_proposal.py
  • synthetic-creativity-archive:agentic_lea_0/run_audit.py
  • synthetic-creativity-archive:agentic_lea_0/run_lea.py
  • synthetic-creativity-archive:agentic_lea_1/run_audit.py
  • synthetic-creativity-archive:agentic_lea_1/run_followup.py
  • synthetic-creativity-archive:agentic_lea_1/run_followup2.py
  • synthetic-creativity-archive:agentic_lea_1/run_lea.py
  • synthetic-creativity-archive:agentic_lea_2/run_audit.py
  • synthetic-creativity-archive:agentic_lea_2/run_lea.py
  • synthetic-creativity-archive:agentic_lea_2b/run_audit.py
  • synthetic-creativity-archive:agentic_lea_2b/run_lea.py
  • synthetic-creativity-archive:agentic_lea_2c/freeze_stage_a.py
  • synthetic-creativity-archive:agentic_lea_2c/run_audit.py
  • synthetic-creativity-archive:agentic_lea_2c/run_stage_a.py
  • synthetic-creativity-archive:agentic_lea_2c/run_stage_a_followup.py
  • synthetic-creativity-archive:agentic_lea_2c/run_stage_a_followup2.py
  • synthetic-creativity-archive:agentic_lea_2c/run_stage_b.py

Evidence record

Artifacts and frozen runs

Result artifacts

  • RESULTS.md
  • RESULTS_QWEN.md

Run records

5 registered runs
  • agentic_lea_0
  • agentic_lea_1
  • agentic_lea_2
  • agentic_lea_2b
  • agentic_lea_2c

Evidence boundary

Formal validity in a supplied or expanded language does not by itself establish mathematical creativity.

This registry links the experiments reported by the three books to their executable or archived code surfaces. A code link establishes traceability, not independent reproduction, correctness, or support for a claim beyond the experiment's stated boundary.