(1/3) The Big Compute of 2026 by OpenAI (and others) offers a kind of empirical evidence in favor of the consistency of mathematics (or rather, whatever axiom system is embedded in Lean).
(2/3) If there were an inconsistency, exploring the tree of implications the way OpenAI did would be a good way to find it!
(3/3) I suggest that for their next stunt, OpenAI should throw a $1,000,000 in tokens into the prompt “Search for a contradiction in math”; if nothing else, this would be a good way to debug Lean or increase our confidence that it is bug-free.
Georg Cantor set out to solve an arcane problem about trigonometric series and ended up revolutionizing mathematics. Along the way he gave the world new ways to think about infinity. See "On Beyond Omega!" at Mathematical Enchantments: mathenchant.wordpress.com/20…
(1/3) I just realized that the reason our universe is three-dimensional rather than two-dimensional is that two-dimensional stat mech models are exactly solvable while three-dimensional ones are not. The connecting link is Douglas Adams’s Second Theory of
(2/3) of Universal Bizarreness and Inexplicability: “There is a theory which states that if ever anyone discovers exactly what the Universe is for and why it is here, it will instantly disappear and be replaced by something even more bizarre and inexplicable.
Here's another dynamic Hamiltonian circuit. This one visits 16 moving points on 8 circles; the points form diameters of the 8 incircles of the faces of an octahedron. The circles alternate rotation direction around each vertex. The circuit has constant length!
A loop joins eight moving points on four circles in such a way that the length of the loop remains constant.
The inspiration for this came from Chuck Hoberman's "Nested Loops" exhibit. I used ChatGPT to search the space of possible solutions in which total length doesn't change (I'm pretty sure that "Nested Loops" lacks this property). youtube.com/watch?v=e4sARevL…
My latest Mathematical Enchantment, "Solving the Flat Cube", describes a new puzzle devised by Oskar van Deventer, Dmitry Andreev, and me, and shows how sometimes you can solve a math problem by adding a dimension OR by throwing a dimension away. mathenchant.wordpress.com/20…
"Nested Loops" is on display at the National Museum of Mathematics in New York City. The exhibit in an easily-overlooked spot, so if you have trouble finding it, ask a docent.
David Kelly is no longer with us (see mathenchant.wordpress.com/20…) but Yellow Pig Seventeen lives on!
The world's worst way of writing the integer four just dropped. See my latest Mathematical Enchantment, "What Bad Bases Are Good For": mathenchant.wordpress.com/20…
Watch a cancer cell drink itself to death, thanks to Dr. Louise Chow’s work on catastrophic macropinocytosis and my daughter Eliana’s animation.
If you like it, please Like it!
youtu.be/jC1R8hSzAqs
In my latest Mathematical Enchantments essay, Seventeen Camels and Where They Can Take You, six seemingly unrelated brain-teasers can be solved using a single elegant trick. mathenchant.wordpress.com/20…
Consider signing the Leiden Declaration:
leidendeclaration.ai/
To take it a step farther, consider joining the \begin{proof} community:
begin-proof.com/





