DkMath — Verifiable AI Mathematical Research

• 

  Number Theory via Cosmic-Style Mathematics

• 

  LEAN Comparator Live: InfinitudeOfPrimes: DkMath.CosmicFormula.euclid_from_cosmic_boundary (n + 1) with ⟨p, hp_ge, hp_prime⟩

Inspiration

DkMath began as a long-running effort to formalize original mathematical structures in Lean 4 while preserving a complete, auditable trail from informal insight to machine-checked proof. The project treats AI as part of a disciplined research loop rather than as an authority: human mathematical direction fixes the contract, GPT-5.6 reviews the mathematics and architecture, Codex investigates and implements at repository scale, Lean verifies every accepted theorem, and Git preserves provenance.

What it does

DkMath is a large formal mathematics research library built on Lean 4 and Mathlib. It contains original definitions, reusable theorem families, proof bridges, examples, development reports, and source-level documentation. Codex can inspect this accumulated mathematical context, discover existing APIs, and extend the library without starting from a blank prompt.

The Build Week project demonstrates the complete workflow through a small but genuine theorem chain:

1. Start with a finite set of known primes.
2. Form their product and add a coprime offset.
3. Prove that any prime factor of the new boundary lies outside the original finite set.
4. Connect that boundary to a Cosmic Formula square-completion identity.
5. Verify a fixed numerical example in Lean.
6. Visualize the same verified data with Manim.

Build Week result

The formal MVP proves a general finite-prime escape theorem and the Cosmic completion identity

P * (P + 2u) + u^2 = (P + u)^2.

The fixed demonstration uses

• S = {2, 3, 5, 7}
• P = 210
• u = 11
• P + u = 221 = 13 * 17

Lean verifies that 13 and 17 divide the completed boundary and are fresh relative to the original finite prime set. A Manim sequence presents the same chain visually, and an FFmpeg-based build pipeline reproduces the final sub-three-minute promo.

New GN5 extension

During final preparation, the finite-prime escape theorem was connected to a fifth-degree Cosmic Formula GN channel:

• {2, 3, 5} has product 30
• 30 + 1 = 31
• 31 = GN(5, 1, 1)
• the escaped prime is exactly 31
• 31^2 does not divide GN(5, 1, 1)
• therefore GN(5, 1, 1) cannot be a perfect fifth power

The implementation packages this as a clean local prime channel and proves the perfect-fifth-power obstruction in Lean. The GN5 extension passed Lean CI, was merged into the main branch, and is included in the DkMath m-v1.0.0 public release.

This is not a proof of Fermat's Last Theorem for exponent 5. It is a verified minimal working model of the local no-lift obstruction required by the larger FLT formalization.

How we built it

The workflow is deliberately separated into layers:

• Human mathematical direction selects the research target and fixes the mathematical contract.
• GPT-5.6 reviews theorem strength, architecture, dependencies, and the next research boundary.
• Codex audits the existing repository, finds the smallest missing bridge, implements Lean proofs, and reports exact build results.
• Lean 4 / Mathlib provides kernel-level verification.
• Git and GitHub Actions preserve provenance and continuously rebuild the accepted code.
• Manim and FFmpeg translate the verified theorem chain into a reproducible visual explanation.

Codex accelerated the work most strongly during repository reconnaissance: instead of re-proving large parts of the library, it found and reused existing finite-product, divisibility, primitive-prime, GN, and no-lift APIs.

Challenges we ran into

The main challenge was not generating code. It was identifying the weakest honest theorem that connected several mature parts of a large formal library without introducing a parallel abstraction hierarchy or overstating the mathematics.

We also had to keep three layers synchronized:

• the general Lean theorem,
• the fixed numerical demo,
• the visual story shown in Manim.

The final video pipeline was designed so that the accepted Manim render can be reused without rebuilding the full graphics environment.

Accomplishments that we're proud of

• A general finite-prime escape theorem with no unfinished proof placeholders.
• A verified Cosmic square-completion theorem.
• A fixed end-to-end demo at 221 = 13 * 17.
• A reproducible Manim and FFmpeg visual pipeline.
• A GN5 clean-channel extension proving that GN(5,1,1) is not a perfect fifth power.
• Full Git history, development reports, exact theorem names, and Lean CI evidence.

Final demo status

The final synchronized and narrated public demo is complete and available on YouTube. It remains under three minutes and explicitly explains what was built, how Codex accelerated repository-scale implementation, and how GPT-5.6 was used for mathematical review, architecture, and communication.

What we learned

AI-assisted mathematics becomes substantially more reliable when every accepted claim is grounded in a formal repository and checked by a proof kernel. The valuable capability is not isolated theorem generation, but sustained understanding of a large, unfamiliar mathematical system and disciplined reuse of verified knowledge.

What's next

The immediate research question is whether the concrete GN5 model can be generalized from GN(5,1,1) to the arbitrary GN 5 u y terms arising in the FLT5 branch. The missing bridge is now sharply identified: construct a finite bad-prime set, force a fresh prime to land in the general GN term, and recover a local no-lift channel. Bounded Cosmic Formula inverse projection remains a separate future direction after this higher-priority FLT5 investigation.

Built With

• ffmpeg
• git
• github-actions
• gpt-5.6
• kokoro-tts
• lean-4
• manim
• mathlib
• openai-codex
• python