6 ms·

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 aggr

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.

danabramov 1y ago
Check out Terence Tao’s book called Analysis. It is sometimes challenging but it opened that world for me.
hobs 1y ago
You probably are vaguely referencing the Principa Mathematica.
- Tainnor 1y ago
  That's a very outdated text that is mostly irrelevant for modern maths except for its historical importance.
treyd 1y ago
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.
- deleted 1y ago
  [deleted]
- cnity 1y ago
  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.
  - RossBencina 1y ago
    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.
    - Waterluvian 1y ago
      Could one possibly use Lean to make up their own mathematical model that is wrong but mostly holds up for a while? Kind of like a Sudoku where it’s all working and then you realize one thing doesn’t work so the rest has to be torn down. I have young kids, and in exploring why boats float I suggested the four elements model. They tested it with bottles full of air and water and earth and it all kind of held up until they found a bowl that floats. Making a wrong model helped the learning process more than telling them the right model. I loved every minute of the science.
      - Tainnor 1y ago
        You can add any axiom you want in Lean and then see what follows (although what follows might be that you prove a contradiction). See the article for details. I don't know if there's a way to remove axioms, nor do I think you can change the logical foundations (which are based in type theory).
ants_everywhere 1y ago
> 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.
- danabramov 1y ago
  >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?
  - ants_everywhere 1y ago
    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.
    - 082349872349872 1y ago
      > It took centuries to realize you couldn't Millennia, even
- RossBencina 1y ago
  > Proofs in algebra often have a satisfying game-like quality. Interesting. I find them banal and deeply unsatisfying.
swagmoney1606 1y ago
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.
- JonChesterfield 1y ago
  Choosing the axioms is difficult.
  - petesergeant 1y ago
    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.
  - deleted 1y ago
    [deleted]
- galaxyLogic 1y ago
  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?
  - deleted 1y ago
    [deleted]
  - sroelants 1y ago
    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.
wging 1y ago
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 https://adam.math.hhu.de/#/g/leanprover-community/nng4
- Waterluvian 1y ago
  How did I miss this! Thanks for pointing it out. This is scratching the itch.
- magicalhippo 1y ago
  Had a blast with that game, really scratched that puzzle itch, and got to relearn some long-forgotten knowledge.
- SilasX 1y ago
  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.
  - derdi 1y ago
    > 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.
jheitmann 1y ago
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 https://steamcommunity.com/app/2262930
deleted 1y ago
[deleted]
hcs 1y ago
Some good mentions elsewhere in the thread, another to check out is The Incredible Proof Machine https://incredible.pm/ https://incredible.pm/
- foooooobar 1y ago
  Fun fact: the author of the The Incredible Proof Machine (Joachim Breitner) also works on Lean :-)
booleandilemma 1y ago
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.
- Waterluvian 1y ago
  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.
Tainnor 1y ago
> 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.
- Waterluvian 1y ago
  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?”
carodgers 1y ago
> 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.

danabramov 1y ago

Check out Terence Tao’s book called Analysis. It is sometimes challenging but it opened that world for me.

hobs 1y ago

You probably are vaguely referencing the Principa Mathematica.

Tainnor 1y ago
That's a very outdated text that is mostly irrelevant for modern maths except for its historical importance.

treyd 1y ago

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.

deleted 1y ago
[deleted]
cnity 1y ago
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.
- RossBencina 1y ago
  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.
  - Waterluvian 1y ago
    Could one possibly use Lean to make up their own mathematical model that is wrong but mostly holds up for a while? Kind of like a Sudoku where it’s all working and then you realize one thing doesn’t work so the rest has to be torn down. I have young kids, and in exploring why boats float I suggested the four elements model. They tested it with bottles full of air and water and earth and it all kind of held up until they found a bowl that floats. Making a wrong model helped the learning process more than telling them the right model. I loved every minute of the science.
    - Tainnor 1y ago
      You can add any axiom you want in Lean and then see what follows (although what follows might be that you prove a contradiction). See the article for details. I don't know if there's a way to remove axioms, nor do I think you can change the logical foundations (which are based in type theory).

ants_everywhere 1y ago

> 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.

danabramov 1y ago
>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?
- ants_everywhere 1y ago
  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.
  - 082349872349872 1y ago
    > It took centuries to realize you couldn't Millennia, even
RossBencina 1y ago
> Proofs in algebra often have a satisfying game-like quality. Interesting. I find them banal and deeply unsatisfying.

swagmoney1606 1y ago

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.

JonChesterfield 1y ago
Choosing the axioms is difficult.
- petesergeant 1y ago
  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.
- deleted 1y ago
  [deleted]
galaxyLogic 1y ago
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?
- deleted 1y ago
  [deleted]
- sroelants 1y ago
  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.

wging 1y ago

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 https://adam.math.hhu.de/#/g/leanprover-community/nng4

Waterluvian 1y ago
How did I miss this! Thanks for pointing it out. This is scratching the itch.
magicalhippo 1y ago
Had a blast with that game, really scratched that puzzle itch, and got to relearn some long-forgotten knowledge.
SilasX 1y ago
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.
- derdi 1y ago
  > 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.

jheitmann 1y ago

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 https://steamcommunity.com/app/2262930

deleted 1y ago

[deleted]

hcs 1y ago

Some good mentions elsewhere in the thread, another to check out is The Incredible Proof Machine https://incredible.pm/ https://incredible.pm/

foooooobar 1y ago
Fun fact: the author of the The Incredible Proof Machine (Joachim Breitner) also works on Lean :-)

booleandilemma 1y ago

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.

Waterluvian 1y ago
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.

Tainnor 1y ago

> 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.

Waterluvian 1y ago
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?”

carodgers 1y ago

> 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.