Comment by Waterluvian
3 days ago
Wait… so are we basically compiling a dictionary of proofs all stemming from a handful of self-evident truths? And every further proof is just some logical aggregation of previous proofs?
Can someone please turn this into a Zachtronics style game?! I badly, direly want this. There’s a game called Euclidea that’s kind of like this for trigonometry and the whole premise of building a tower of logic is deeply attractive to me.
Is this what pure math is about? Is this what people who become math profs are feeling in their soul? The sheer thrill of adding to that dictionary of proofs?
Aside: I recall some famous mathematician had made a list of base proofs that you just hold to be true. Can someone remind me who, and/or what that list is called? I’m guessing they’re considered axioms.
There is a game already, though it may not be exactly what you want (and the goal is definitely not "generate all known math"). I've played around with it, and I do think it's pretty fun.
The article mentions it, in fact: https://adam.math.hhu.de/#/g/leanprover-community/nng4
How did I miss this! Thanks for pointing it out. This is scratching the itch.
Had a blast with that game, really scratched that puzzle itch, and got to relearn some long-forgotten knowledge.
I played through a lot of it, and while it was fun, I wouldn't call it gamified in the sense that Zachtronics does it. As an FYI, here are some sticking points I ran into as well:
1) It uses the term "goal" for the the current stage of the proof you're working on, which is counterintuitive. In common speech, the goal is the theorem you're trying to prove, not the current step you're on in proving it. It would be like if I were helping you get to work in the morning, and I said, "Okay, you're current [sub]goal is that you're done brushing your teeth." No. That's not a goal. That's progress toward a goal.
2) It doesn't warn you early on about the left-associativeness of the operator binding, or what to do about it. So you can apply what seem like valid transformations but then parentheses pop up that you don't expect, and which you have no guidance on how to deal with. I had to ask ChatGPT what was going on to solve it.
> It would be like if I were helping you get to work in the morning, and I said, "Okay, you're current [sub]goal is that you're done brushing your teeth." No. That's not a goal. That's progress toward a goal.
Interesting. Let's say our overall goal is to get to work showered, wearing clean clothes, and having brushed our teeth. After we showered and put on clean clothes, wouldn't you say that the remaining goal is to brush our teeth and get to work? And if we then do brush our teeth, wouldn't you say that the remaining goal is to get to work? In this scenario, if anything can be called progress, it is what's in the past (the showering etc.), not what is still to be done.
1 reply →
> Can someone please turn this into a Zachtronics style game?!
That game is called math :) Partially joking, but I do think a game version would be fun.
> Is this what pure math is about?
More or less yes for an undergrad, but when you get to research it feels different.
> I badly, direly want this
Consider checking out an abstract algebra book. Maybe Dummit and Foote or something else popular. Proofs in algebra often have a satisfying game-like quality. The more popular books will have solutions you can find online if you get stuck.
>More or less yes for an undergrad, but when you get to research it feels different.
Would you mind telling more about how it feels different in research?
You can get into a meditative zone when you're manipulating equations using techniques you've internalized.
In research you're doing a lot more of things like reading papers, putting your thoughts into words, trying to understand something the author of the paper barely understands, feeling lost and unsure where to look next. All of that can feel good too (or it cannot depending on the person) but it's a different feeling than playing a logic game.
As one example, Euclidia is a fun meditative game. But compare the difference in feeling between doing an exercise from Euclid and trying to prove the parallel postulate. It took centuries to realize you couldn't prove it, and then there was a lot of hard work trying to figure out what geometry was like if you get rid of it.
1 reply →
> Proofs in algebra often have a satisfying game-like quality.
Interesting. I find them banal and deeply unsatisfying.
That's fine. Different people prefer different subjects. But IME the mode graduate student finds algebra to be an enjoyable class because of the proofs.
You might be thinking of Euclid's axioms, which defines points, lines, planes, etc, and that lines can be parallel. This is an interesting one because the system is violated if your space is not flat, like if you're on a sphere.
You could also be thinking of Zermelo-Fraenknel set theory (ZF/ZFC), which most of modern mathematics is ultimately based upon.
This highlights I think what is an ultimate pitfall of something like Lean. It is something like this: when an assumption is broken or violated in mathematics, the whole field of mathematics can _grow_. Non-euclidean geometry, imaginary numbers, etc are all examples of this. Trying to cram maths into a programming language sounds like it would constrain it, removing the creativity and reducing all maths to a search space.
Lean does not reduce the mathematical search space as you suggest. Yes there is a fixed, compact low-level logical core that everything above it depends on. But this is equivalent to an encoding of the logical foundations that mathematics, that formal mathematics depends on in any case. On top that you have mathematical theories built on assumptions (axioms) and you can specify whatever axioms you like and change them at will. To use your analogy: the "search space" is parameterised by user-defined sets of axioms and assumptions.
5 replies →
Check out the game Bombe [1]. It's a minesweeper variant where instead of directly flagging or uncovering cells, you define rules for when cells can be flagged. As it gets more advanced you end up building lemmas that implicitly chain off each other. Then as _you_ get more advanced (and the game removes some arbitrary restrictions around your toolset) you can generalize your rules and golf down what you've already constructed.
[1] https://steamcommunity.com/app/2262930
In my mind this is literally what math is. We start with axioms, and derive conclusions. There's probably more to it than that, but that's the understanding I'm at now.
But shouldn't it also be part of the axioms what are the rules that allow you to derive new theorems from them?
So then you could self-apply it and start ... deriving new rules of how you can derive new theorems and thus also new rules, from axioms?
I'm jusr confused a bit about "axioms" and "rules". What's the difference?
The rules that you use to compose axioms and propositions are a different set of axioms defined by the Logic system you're using. e.g., can a proof consist of infinitely many steps? Can I use the law of excluded middle? Some logic systems won't let you re-use the same proposition more than once, etc,...
They're usually considered separate, because they're orthogonal to the foundational axioms you're using to build up your mathematical systems. With the exact same system of axioms, you might be able to prove or disprove certain things using some logic systems, but not others.
Choosing the axioms is difficult.
Presumably made easier by something like Lean where you can have a very minimal set of axioms, because things you might use as axioms already have proved versions, in Lean.
> so are we basically compiling a dictionary of proofs all stemming from a handful of self-evident truths
I would say, "from a handful of axioms".
It's certainly true that when Euclid started this whole enterprise, it was thought thax axioms should be self-evident. But then, many centuries later, people discovered that there are other interesting geometries that don't satisfy the same axioms.
And when you get to reasoning about infinities, it's very unclear that anything about them can be considered self-evident (a few mathematicians even refuse to work with infinities, although it's definitely a very niche subcommunity).
Some of today's common axioms are indeed self-evident (such as "you should be able to substitute equal subterms"), but things like the axiom of choice have (at least historically) been much more controversial. I would probably say that such axioms can be considered "plausible" and that they generally allow us to be able to prove what we want to prove. But you'll definitely find mathematicians championing different axioms.
> Aside: I recall some famous mathematician had made a list of base proofs that you just hold to be true. Can someone remind me who, and/or what that list is called? I’m guessing they’re considered axioms.
That would be the ZFC axioms. It was originally the ZF axioms (named so after the mathematicians Zermelo and Fraenkel who worked in the early 20th century), and then later the Axiom of Choice (C) was added. It's generally considered to be the "standard" set of axioms for maths, although very few mathematicians actually work directly from these axioms. But in theory, you can take almost every mathematical proof (unless it's explicitly set in some other foundation) and recast it entirely in applications of the ZFC axioms.
Thanks for this. So I have half a thought I’m trying to flesh out from what you’ve shared. Bear with me, whoever reads this:
Are there essentially two flavours:
- the maths based on axioms that are fundamentally, cosmically true such as x = x. And in doing so we’re formalizing on paper the universal truths and all subsequent rules we know to be true given these
- the maths that incorporate those plus additional axioms that aren’t necessarily fundamentally true (or maybe just not provable), but work very well at laying a foundation for further rules that build a practically useful, but not necessarily “correct” toolbox
With the latter, is it kind of a “they won’t hold up under normal conditions but if you accept these axioms, there’s interesting things you can explore and achieve?”
A thing to realize here is that there is no "fundamentally, cosmically true" in math. While math can be used to model reality, it is not bound by reality.
The only thing that matters is what you choose to take as granted for a particular question.
It's like how you can draw a map of a place that doesn't exist.
Or like coming up with rules for a game and then trying it to see how it plays.
Or it's like a material used for construction. You can build a house out of it, but there's no inherent "houseness" to it, despite how common such a use is.
The first set is the rules of logic, which applies in non math stuff too. From there you can add new axioms for boolean logic, for integers, for sets, for geometry, whatever.
Even given that separation (which itself is fuzzy), even the first group can't be construed as "universally true". For example there's a range of opinion around the law of the excluded middle (whether "P is not false" implies "P is true"). Most other propositional logic axioms like modus ponens are less controversial though.
As far as real world math, while ZF set theory axioms are generally viewed as the "foundation", that's due to convention more than any real primacy of ZF. Other set theories and types of "foundations" exist that seem to be just as suitable to be called a "foundation", and most math is "foundation" agnostic. Like, if all you're doing is something with prime numbers, then it doesn't matter what "foundation" you use; so long as it lets you define prime numbers, that's all that matters.
"Foundations" only come into play when you're doing really subtle things with different orders of infinities. And then, yes, the answer can be different depending on what foundation you choose. And that's fine. It doesn't mean that either foundation is wrong. They're just different. Which is why "foundation of mathematics" is a bit of a misnomer / fool's errand. Different foundations have different results on certain edge cases, and those are interesting to investigate, not something to be upset about. And like I said, most "ordinary" math is pretty foundation agnostic.
I would maybe rephrase it as: there are certain axioms that absolutely nobody reasonable takes issue with and then there are others that are more controversial, although it's still important to note that the vast majority of mathematicians accept the ZFC axioms + classical logic.
> Aside: I recall some famous mathematician had made a list of base proofs that you just hold to be true. Can someone remind me who, and/or what that list is called? I’m guessing they’re considered axioms.
Take a look at zeroth-order logic.
Some good mentions elsewhere in the thread, another to check out is The Incredible Proof Machine https://incredible.pm/
Fun fact: the author of the The Incredible Proof Machine (Joachim Breitner) also works on Lean :-)
Check out Terence Tao’s book called Analysis. It is sometimes challenging but it opened that world for me.
You probably are vaguely referencing the Principa Mathematica.
That's a very outdated text that is mostly irrelevant for modern maths except for its historical importance.
How are you asking questions like this and yet you're a roboticist and a principal software engineer in the autonomous mobile robotics industry.
From your questions I marked you as a high schooler.
Probably similar to how numerous maths PhDs I’ve worked with are terrible at shipping durable production code on time and on budget, or how many doctors are terrible at inserting IVs, or how an architect may likely be terrible at framing a house, or how some Grammy winning musicians can't read classical notation: your mental model for domains of expertise is probably wrong.