Building an open-source virtual mathematical kernel with Lean4 for solving enumerative geometry problems
(Note: The classical Chow relation traditionally relies on graded rings over complex numbers. This project clarifies and addresses that gap by developing a generalized framework not dependent on complex numbers.) We call this framework virtual set theory (note this is a research project timelines at the end of this document).
One the ethical use of AI for this project: All concepts and calculations are done manually, some use of LLMs will be used to speed up development and boostrap formal verification in Lean4. Results will be published on ArXiv for peer-review. Open contributions are welcome.
We address the Problem of Apollonius and its generalizations by introducing a rigorous reformulation of set membership within an appropriate moduli space (\mathcal{M}), unifying points, lines, and circles under a single geometric framework. Enumerating degenerate tangency conditions and recasting tangency constraints as intersection relations, we obtain a parametrized equation for solution counts involving unknown coefficients (\alpha) and (\beta).
A central tool in enumerative geometry is the Chow ring relation (h^3 = 2h), which encodes multiplicity patterns of triple intersections on moduli spaces. It is well-established that this relation holds rigorously only for graded rings derived from complex algebraic geometry over algebraically closed fields. This classical applicability creates a fundamental gap when working over (\mathbb{R}) or non-graded rings, such as with our moduli space (\mathcal{M}) of points, lines, and circles.
Our project explicitly addresses this gap by extending intersection-theoretic computations beyond classical complex settings:
- We introduce virtual intersection multiplicities (\alpha) and (\beta) accounting for fractal degenerations and singularities not captured by classical algebraic geometry.
- We formulate and solve independent algebraic relations for these multiplicities derived from global geometric invariants and deformation-obstruction theory.
- Our Virtual Set Theory (VST) framework generalizes classical membership to a recursive, fractal-parameterized relation, enabling well-defined intersection theory in analytic and fractal moduli contexts without requiring complex numbers.
- Thus, we recover and generalize the Chow relation as part of a corrected virtual intersection framework compatible with real-analytic moduli spaces.
This allows a rigorous enumerative solution (count of 17 tangent circles) to the generalized Apollonius problem without dependence on complex algebraic geometry, bridging foundational gaps in classical approaches.
Our project develops a rigorously validated virtual mathematical kernel built on the Virtual Set Theory framework, implemented in Lean 4. This kernel provides foundational tools to solve enumerative geometry problems using uniform core machinery, supporting mathematical rigor and computational feasibility.
Notably, our approach does not require the classical Chow ring relation to hold in the strict algebraic-geometric sense but instead incorporates virtual multiplicities to extend intersection theory beyond complex graded rings.
Image: Ludwig Feuerbach
"A circle in a straight line is the mathematical symbol of miracle." — Ludwig Feuerbach, The Essence of Christianity
Using Lean 4, we formalize all axioms, definitions, and theorems underlying our approach, enabling computer-verified proofs of enumerative results including Apollonius problems. The project roadmap envisions extending beyond current minimal examples to a broad class of enumerative geometry challenges.
The source code is available on GitHub: Virtual Set Theory Repository
axioms.lean— Foundational axioms including classical and virtual membership.definitions.lean— Uniform definitions of points, lines, circles in moduli space (\mathcal{M}).theorems.lean— Major theorems and intersection relations, including the generalized Chow relation with virtual multiplicities.apollonius.lean— Main kernel for the enumerative Apollonius problem, incorporating virtual set membership.
Classical set theory and algebraic geometry provide foundational tools for enumerative geometry problems but face limitations when handling fractal degenerations and recursive constraints inherent in many NP-hard generalizations, such as the Apollonius problem.
A core limitation is that the classical Chow ring intersection relations, such as (h^3 = 2h), hold strictly in the context of graded rings over complex numbers and smooth projective varieties. Our moduli space (\mathcal{M}), defined over (\mathbb{R}), includes singularities, degenerations, and non-algebraic contexts where these classical relations do not apply directly.
Virtual Set Theory (VST) addresses this by:
- Generalizing membership to a recursive, parameterized fractal relation reflecting the stratified structure of the moduli space.
- Introducing virtual intersection multiplicities accounting for degenerate and fractal contributions.
- Establishing a corrected intersection theory extending Chow ring computations beyond the classical complex setting.
- Providing a rigorous, computer-verified proof framework in Lean 4 to validate enumerative counts without depending on complex number assumptions.
The moduli space
[ \mathcal{M} = {(x,y,r) \mid (x,y) \in \mathbb{R}^2, r \in \mathbb{P}^1(\mathbb{R}) = \mathbb{R} \cup {\infty}} ]
encodes:
- (r=0): points,
- (r \in (0, \infty)): circles,
- (r=\infty): lines,
uniformly within a real-analytic, stratified geometric space supporting both classical and degenerate elements.
-
The classical Chow ring relation
[ h^3 = 2h, ]
which counts triple tangencies, is valid primarily in graded rings associated to complex algebraic varieties.
-
In our real-analytic and fractal geometric context, this relation does not hold directly due to lack of grading, lack of algebraic closure, and analytic degenerations.
-
Instead, we introduce virtual multiplicities (\alpha, \beta) to parametrize deviations from classical multiplicities:
[ (3h^2 - \alpha h^3)(2h - \beta h^2)(12 h^3 - 20 h^2) ]
-
By developing and solving a system of algebraic equations relating (\alpha), (\beta) derived from virtual fundamental classes and deformation-obstruction theory, we effectively recover an extended Chow ring relation suited to (\mathcal{M}).
- We encode tangent counts via divisors (h) on (\mathcal{M}).
- Intersection products reflect combined constraints.
- Applying the corrected virtual Chow relation with multiplicities (\alpha, \beta), we derive explicit counts.
- Solving the resulting equations rigorously confirms the total count of 17 solution circles (matching classical enumerations for Apollonius but extended through virtual intersections).
Replacing classical binary membership
[ x \in A, ]
we define parameterized virtual membership
[ \widetilde{\in}: E \times \mathcal{I} \to {0,1}, ]
where (E) is the universe of geometric elements and (\mathcal{I}) is a stratified indexing space reflecting recursive fractal structure.
This relation enables a controlled embedding of classical sets into a virtual universe that supports recursive fractal degenerations and resolves foundational paradoxes without restricting to classical Foundation axioms.
| Phase | Goals | Timeline |
|---|---|---|
| Foundations | Formalize recursive membership; prove consistency; resolve paradoxes | 2025 Q4 – 2026 Q2 |
| Moduli and Chow | Construct (\mathcal{M}); define divisors; prove generalized Chow relation with (\alpha, \beta) | 2026 Q3 – 2027 Q1 |
| Extensions | Higher-dimensional moduli; recursive invariants; embeddings in homotopy/derived settings | 2027 Q2 – 2027 Q4 |
| Foundations Refining | Ship of Theseus morphisms; categorical embeddings; workshops and publications | 2028 |
- Fulton, W. Intersection Theory, Springer, 1998.
- Gitman, V., Hamkins, J.D., Wilson, J. "Virtual large cardinals," Journal of Symbolic Logic, 2020.
- McKean, K. "Recent advances in enumerative geometry," arXiv:2210.13288, 2022.
- Lurie, J. Higher Topos Theory, 2009.
- Voevodsky, V. Homotopy type theory: Univalent foundations, 2013.
Virtual Set Theory is a meta-framework enabling systematic extension of classical mathematics via recursive, fractal virtual membership relations. It is implemented and formally verified in Lean 4 to support rigorous enumerative geometry beyond classical algebraic geometry.
Collaboration and feedback are warmly welcomed via the GitHub repository:
https://github.com/EnumerativeGeometry/enumerativegeometry.github.io
Best regards,
Yesod Bourbansky