You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Anthony Bordg (Apr 25 2026 at 17:02):Dear CT users,
Two preprints about AlphaGeometry, sharing in the first one some perspectives on its foundations, its soundness (or lack thereof), its potential extension through (higher-order) signatures, and in the second one unearthing a log-linear bottleneck in its synthetic data generation pipeline, and sharing some new perspectives on how to peer into the mechanistic interpretability of its latent space by testing the invariance of its input space using an old and well-known duality between logic and topology.
This is open-source and may be of interest to some of you.
Some pointers:
The accompanying code of the above preprint:
-- GitHub UI: https://github.com/AnthonyBordg/beyond-the-plane/tree/v1.0.0
-- Frozen Zenodo: https://doi.org/10.5281/zenodo.19238761
The Topological Dual of a Dataset: A Logic-to-Topology Encoding for AlphaGeometry-Style Data, https://doi.org/10.5281/zenodo.18961053
cheers,
Anthony
Morgan Rogers (he/him) (Apr 26 2026 at 18:48):Obvious question: what is AlphaGeometry?
John Baez (Apr 26 2026 at 19:25):Here's what Google researchers wrote in a paper published in Nature in 2024:
Proving mathematical theorems at the olympiad level represents a notable milestone in human-level automated reasoning[1,2,3,4], owing to their reputed difficulty among the world’s best talents in pre-university mathematics. Current machine-learning approaches, however, are not applicable to most mathematical domains owing to the high cost of translating human proofs into machine-verifiable format. The problem is even worse for geometry because of its unique translation challenges[1,5], resulting in severe scarcity of training data. We propose AlphaGeometry, a theorem prover for Euclidean plane geometry that sidesteps the need for human demonstrations by synthesizing millions of theorems and proofs across different levels of complexity. AlphaGeometry is a neuro-symbolic system that uses a neural language model, trained from scratch on our large-scale synthetic data, to guide a symbolic deduction engine through infinite branching points in challenging problems. On a test set of 30 latest olympiad-level problems, AlphaGeometry solves 25, outperforming the previous best method that only solves ten problems and approaching the performance of an average International Mathematical Olympiad (IMO) gold medallist. Notably, AlphaGeometry produces human-readable proofs, solves all geometry problems in the IMO 2000 and 2015 under human expert evaluation and discovers a generalized version of a translated IMO theorem in 2004.
Todd Trimble (Apr 26 2026 at 20:41):Euclidean plane geometry, formalized by suitable first-order axioms by following Tarski (for example), is a decidable theory. (This is closely related to the decidability of the theory of real closed fields.) So roughly speaking, there is an algorithm which, upon being fed a sentence in Euclidean plane geometry, will produce a proof of the sentence if it is true, and a proof of its negation if it is false. However, the algorithm can be very slow.
(This reminds me of a nice post by @Chris Grossack (she/they) on competition-type problems about the real plane that can be phrased in the language of ordered fields, and getting Sage to "slaughter" them, by exploiting quantifier elimination methods, which are due to Tarski originally.)
I'm mildly curious to what extent AlphaGeometry engages with quantifier elimination methods.
Morgan Rogers (he/him) (Apr 28 2026 at 07:43):Follow-up question: what relation to category theory?