We formalized the proof of the 3D Kakeya conjecture in Lean from the Sticky Kakeya theorem. Together with the unconditional Sticky Kakeya formalization by Nankai University × ByteDance Seed AI4Math, this gives a complete formal proof with no sorry and no project-specific mathematical axiom. A great example of how AI can help turn frontier mathematics into machine-verified proofs. github.com/project-numina/ka… github.com/M32026/3d-sticky-… projectnumina.ai/article?slu… @ProjectNumina @GanjinZero

Standing on the shoulders of giant AI models, we utilize accessible models (Claude/Gemini/GPT-5.2) with a novel agentic reasoning loop. The Brascamp-Lieb formalization (arXiv:2511.11091) took just 2 weeks. This demonstrates concurrent autoformalization: providing machine-checked guarantees while a paper is still under peer review.

This progress is built on the foundational work of the @Mathlib community. The future of math research lies in transparent tools that amplify human insight. We are hiring Mathlib experts to join this effort. Apply: [email protected]

Announcing Numina-Lean-Agent: an open-source framework achieving SOTA in formal theorem proving using generic models. Two major breakthroughs: 🏆 12/12 on Putnam 2025 📜 Formalized the "Effective Brascamp-Lieb inequalities" research paper (>90% AI-generated) Code: github.com/project-numina/nu… Demo: demo.projectnumina.ai/ Paper: github.com/project-numina/nu…