6 ms·

Will Computers Redefine the Roots of Math?

54 points by ykonstant 3y ago

zmgsabst 3y ago
I think the intuition behind HoTT is truly fascinating: The topology of (category) diagrams can represent a type theory’s semantics — and equivalence in your theory is a question about paths in diagrams. An application of the idea that topology connects “algebra” (type theory) to “geometry” (diagrams composed of cells).
- maxiepoo 3y ago
  It really is remarkable. I think the most remarkable fact about it is that the intensional identity type was invented by Martin Lof in the 70s, the groupoid model was discovered in the 90s and then finally in the late 2000s various people made the connection that Martin Lof's original system from the 70s was in a sense already a type theory for abstract homotopy theory. This led to an explosion of new ideas in type theory (univalence, higher inductive types, modalities) that took a somewhat obscure field of math/cs to the thriving research community it is today.
  - zmgsabst 3y ago
    I’ll admit to coming late to the party (when a friend introduced me in 2013), but what’s amazing to me is when you take the step of encoding your cellular structures as adjacency matrices. You can visually see structures of your theory (eg, facts about groups) in the patterns of terms in the matrix. Eg, diagramming a cyclic group ends up with a banding pattern in the portion of your matrix denoting equivalent pairs under the operation… which shows that in some sense, the level maps of + on Zn x Zn form a twisted torus. (Which makes sense in hindsight, as you have the product of two loops with the level maps wrapping around non-trivially.) That you get ideas such as that by chasing through a purely abstract definition (groups -> diagrams) is wild to me. Edit: I actually built a simple case (Z4) in Minecraft — just because I found it surprising. https://zmichaelgehlke.com/images/z4-plus-map.png https://zmichaelgehlke.com/images/z4-plus-map.png And you get all kinds of weird visuals in diagrams. Like “log” or “exponential” curves trying to diagram a whole field. (Z5, in this case.) https://zmichaelgehlke.com/images/5-finite-field.png https://zmichaelgehlke.com/images/5-finite-field.png
practal 3y ago
Yes.
1970-01-01 3y ago
Aren't the 'roots of math' fully empirical and inclusive of all sets? How can roots be changed without a redo of the universe?
- maxiepoo 3y ago
  > How can roots be changed without a redo of the universe? This is a very interesting question and I think reflects a mismatch between how we commonly think about of foundations of mathematics and what role foundations actually play in mathematics. There's no recording online but I recommend looking at the slides to Mike Shulman's talk from JMM 2022 where he discusses this point: http://sigmaa.maa.org/pom/Slides/shulman-2022jmm.pdf http://sigmaa.maa.org/pom/Slides/shulman-2022jmm.pdf . Mike works on, among other things, homotopy type theory, the subject of the original article. His basic point is that we should think of math more like programs that we can "compile" to various backends. If your math is high level it's not necessarily tied to a particular "architecture" like ZFC.
- zmgsabst 3y ago
  Math isn’t empirical: it’s assumed axioms which define a formal system. One way to do that is set theory. Another is category theory. A third way is type theory. We try to pick a set of assumptions that allow us to use the language to reason about the world around us — a modern ontology. But is the Banach-Tarski paradox a fact about the real world? — or merely a part of the game we play? Hard to know. https://en.wikipedia.org/wiki/Banach–Tarski_paradox https://en.wikipedia.org/wiki/Banach–Tarski_paradox
  - staunton 3y ago
    > Math isn’t empirical: it’s assumed axioms which define a formal system. There are mathematicians who would disagree. They would say that math is discovered, not invented and that axioms don't actually matter. They would also say that mathematicians may study axioms using mathematical methods but need not base their methods on axioms or formal systems. They would say that you can switch out your foundations and have the same math for all purposes you care about (if you don't care about axioms). While I don't agree with everything there, I think they definitely make a point that's worth thinking about. For example, very few mathematicians would be able to spell out from memory "their basic axioms" (maybe ZFC, category theory, etc., maybe they don't even know or care, or switch depending on context). Now why is that? Their work is so far removed from foundations that they don't have to care. They will rightfully demand that their theorems and ways of reasoning be supported by the axioms. Beyond that, you can tinker and change them all you please. They only need a small part of your foundations to do their work. Crucially, most of them wouldn't "waste" their precious time on e.g. "formalizing that minimal foundation". Maybe one could view foundations as a bunch of programming languages where using the high level features looks indistinguishable and almost noone uses the low-level. I think this intuition strongly suggests that eventually computers will win and all mathematicians will use proof systems (maybe without even knowing how they work under the hood). That is, until maybe the machines surpass their reasoning ability so much that humans are obsolete in that space.
dwheeler 3y ago
If you're interested in formalizing math, check out Metamath: https://us.metamath.org https://us.metamath.org. By itself Metamath doesn't embed any particular set of axioms. The most widely used database (axioms and proven theorems) uses classical logic and set theory, but there's also databases for intuitionistic set theory, new foundations, and higher order logic.
- panabee 3y ago
  thanks so much. this is extremely useful and could help in training a specialized model for math and logic.
c7b 3y ago
Great read, I was expecting it to bring up the four color theorem, but it was actually an even more interesting debate touching on some modern mathematics. I think it's still worth bringing it up: https://en.m.wikipedia.org/wiki/Four_color_theorem https://en.m.wikipedia.org/wiki/Four_color_theorem In a nutshell, they proved that all maps of contiguous countries can be colored using only four colors by reducing the infinite set of possible maps to a finite one and then having a computer check each case. In the 70's, this wasn't considered a 'real' proof, and it was argued that we can't trust the machine the way we can trust human mathematicians. My first reaction upon hearing about that debate was similar to what probably most HN readers would think, that it's arguably the other way round and we should ideally only trust proofs that had been fully formalized by machines. Glad to see that we're making progress in this direction. Also worth mentioning: apart from Coq that was discussed in the article, there's also the Lean theorem prover that also features some more general programming elements, it's regularly discussed on HN: https://news.ycombinator.com/item?id=36107796 https://news.ycombinator.com/item?id=36107796 https://news.ycombinator.com/item?id=34456573 https://news.ycombinator.com/item?id=34456573
- Animats 3y ago
  > In the 70's, this wasn't considered a 'real' proof. I ran into that decades ago. We used the original Boyer-Moore theorem prover [1] as part of a program verification system. The system had two provers, the Nelson-Oppen simplifier (the first SAT solver) to automatically handle the easy proofs, and the Boyer-Moore system for the hard ones. To make sure that both had consistent theories, I used the Boyer-Moore prover to prove the "axioms" of the Nelson-Oppen system, especially what are usually called McCarthy's axioms (the ones that use Select and Store) for arrays. The Boyer-Moore system uses a strictly constructive approach to mathematics. It starts from something like Peano arithmetic (there is a number zero, and an operation add 1) and builds up number theory. So I added a concept of arrays, represented as (index, value) tuples in sorted order, and was able to prove the usual "axioms" for arrays as theorems. The machine proofs were long and involved much case analysis.[2] I submitted a paper to JACM in the early 1980s and got back reviews saying that it was just too long and inelegant to be at the fundamentals of computer science. That might not be the case today. A few years back, I put the Boyer-Moore prover on Github, after getting it to work with Gnu Common LISP. So you can still run all this 1980s stuff. It's much faster today. It took about 45 minutes to grind through these proofs on a VAX 11/780 in the early 1980s. Now it takes about a second. The proof log [2] is amusing. It's building up number theory from a very low level, starting by proving that X + 0 = X. Each theorem proved can be used as a lemma by later theorems, so you guide the process by giving it problems to solve in the right order. By line 1900, it's proving that multiplication distributes over addition. Array theory, the new stuff, starts around line 2994. The reason this is so complicated and ugly is that there's no use of axiomatic set theory. Arrays are easy if you have sets. But there are no sets here. Sets don't fit well into this strict constructive theory, because EQUAL means identical. You can't create weaker definitions of equality which say that two sets are equal if they contain the same elements regardless of order, because that introduces a risk of unsoundness. Effort must be put into keeping the tuples of the array representation in ascending order by subscript, which implies much case analysis. Mathematicians hate case analysis. Computers are good at it. [1] https://github.com/John-Nagle/nqthm https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temporaryrulebaseprooflog.txt https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
TechBro8615 3y ago
> “The drive to mechanize proof and proof verification doesn’t strongly motivate most mathematicians as far as I can tell,” he [Michael Harris] said. “I can understand why computer scientists and logicians would be excited, but I think mathematicians are looking for something else.” I'm not a mathematician, but I have at times been able to consider myself a computer scientist. To me, the goal of "mechanizing" and formalizing mathematics seems instinctively recognizable as a worthwhile pursuit, for the same reason it's worth adding tests to an unwieldy legacy codebase: it makes it possible to refactor, to experiment and break things and see what happens. The more we formalize the most fundamental axioms and theorems of mathematics, the more confidently we can alter or remove them and see what happens to the rest of the system. Achieving "100% test coverage" and "instrumentation" of mathematics would allow us to analyze the system under stress. We could fuzz it. We could refactor it. We could even ask an AI to do that for us. As a relative layman, I'm often struck by how many mathematical theorems are dependent on the arbitrary paths we took to develop them. For the same reason, it's a common occurrence that one mathematician discovers an innovation in one branch of mathematics by simply borrowing a common technique from a distantly related branch. Those sorts of analogies and connections between ideas are difficult for humans to spot, and their discovery scales linearly with the number of mathematicians, who might prefer to spend their time discovering truly new ideas rather than repurposing those already existing ideas. But computers, on the other hand, are excellent at spotting these relationships, if given sufficiently formalized definitions of them. So that's why I'd be most excited about formalizing mathematics: how much low-hanging fruit is waiting to be discovered by computers that are just missing the right prompt?
- giraj 3y ago
  Most mathematicians aren't interested in refactoring their mathematical "codebase", nor experimenting with axioms. They simply want to understand and discover more math. The reasons you state for your interest in formalisation don't appeal to most mathematicians. Concerning analogies and borrowing techniques between fields, this is absolutely something humans are good at and which it is very hard for computers to do. Why do you think otherwise? To take a very simple example, most mathematical objects can be represented in different ways. A mathematician can fluently move between these representations, whereas computers cannot. This is a largely the obstacle for the adoption of proof assistants among mathematicians.
giraj 3y ago
For those interested in formalisation of homotopy type theory, there are several (more or less) active and developed libraries. To mention a few: UniMath (https://github.com/UniMath/UniMath https://github.com/UniMath/UniMath, mentioned in the article) Coq-HoTT (https://github.com/HoTT/Coq-HoTT https://github.com/HoTT/Coq-HoTT) agda-unimath (https://unimath.github.io/agda-unimath/ https://unimath.github.io/agda-unimath/) cubical agda (https://github.com/agda/cubical https://github.com/agda/cubical) All of these are open to contributions, and there are lots of useful basic things that haven't been done and which I think would make excellent semester projects for a cs/math undergrad (for example).
deleted 3y ago
[deleted]
dboreham 3y ago
Odd choice of article title. It appears to be about the well known field: "foundations of mathematics", and is even in a section of the web site named "foundations of mathematics". Meanwhile the word "root" doesn't appear anywhere in the article.
- hgsgm 3y ago
  And more unfortunately, the "roots" of mathematics always lead to nothing (0).
cubefox 3y ago
(2015) Unfortunately, Voevodsky, the "hero" of this piece, died in 2017.
orlandpm 3y ago
(2015)
- b215826 3y ago
  Yes, and Voevodsky is no longer alive.
deleted 3y ago
[deleted]

54 points by ykonstant 3y ago

I think the intuition behind HoTT is truly fascinating: The topology of (category) diagrams can represent a type theory’s semantics — and equivalence in your theory is a question about paths in diagrams. An application of the idea that topology connects “algebra” (type theory) to “geometry” (diagrams composed of cells).

maxiepoo 3y ago
It really is remarkable. I think the most remarkable fact about it is that the intensional identity type was invented by Martin Lof in the 70s, the groupoid model was discovered in the 90s and then finally in the late 2000s various people made the connection that Martin Lof's original system from the 70s was in a sense already a type theory for abstract homotopy theory. This led to an explosion of new ideas in type theory (univalence, higher inductive types, modalities) that took a somewhat obscure field of math/cs to the thriving research community it is today.
- zmgsabst 3y ago
  I’ll admit to coming late to the party (when a friend introduced me in 2013), but what’s amazing to me is when you take the step of encoding your cellular structures as adjacency matrices. You can visually see structures of your theory (eg, facts about groups) in the patterns of terms in the matrix. Eg, diagramming a cyclic group ends up with a banding pattern in the portion of your matrix denoting equivalent pairs under the operation… which shows that in some sense, the level maps of + on Zn x Zn form a twisted torus. (Which makes sense in hindsight, as you have the product of two loops with the level maps wrapping around non-trivially.) That you get ideas such as that by chasing through a purely abstract definition (groups -> diagrams) is wild to me. Edit: I actually built a simple case (Z4) in Minecraft — just because I found it surprising. https://zmichaelgehlke.com/images/z4-plus-map.png https://zmichaelgehlke.com/images/z4-plus-map.png And you get all kinds of weird visuals in diagrams. Like “log” or “exponential” curves trying to diagram a whole field. (Z5, in this case.) https://zmichaelgehlke.com/images/5-finite-field.png https://zmichaelgehlke.com/images/5-finite-field.png

practal 3y ago

Yes.

1970-01-01 3y ago

Aren't the 'roots of math' fully empirical and inclusive of all sets? How can roots be changed without a redo of the universe?

maxiepoo 3y ago
> How can roots be changed without a redo of the universe? This is a very interesting question and I think reflects a mismatch between how we commonly think about of foundations of mathematics and what role foundations actually play in mathematics. There's no recording online but I recommend looking at the slides to Mike Shulman's talk from JMM 2022 where he discusses this point: http://sigmaa.maa.org/pom/Slides/shulman-2022jmm.pdf http://sigmaa.maa.org/pom/Slides/shulman-2022jmm.pdf . Mike works on, among other things, homotopy type theory, the subject of the original article. His basic point is that we should think of math more like programs that we can "compile" to various backends. If your math is high level it's not necessarily tied to a particular "architecture" like ZFC.
zmgsabst 3y ago
Math isn’t empirical: it’s assumed axioms which define a formal system. One way to do that is set theory. Another is category theory. A third way is type theory. We try to pick a set of assumptions that allow us to use the language to reason about the world around us — a modern ontology. But is the Banach-Tarski paradox a fact about the real world? — or merely a part of the game we play? Hard to know. https://en.wikipedia.org/wiki/Banach–Tarski_paradox https://en.wikipedia.org/wiki/Banach–Tarski_paradox
- staunton 3y ago
  > Math isn’t empirical: it’s assumed axioms which define a formal system. There are mathematicians who would disagree. They would say that math is discovered, not invented and that axioms don't actually matter. They would also say that mathematicians may study axioms using mathematical methods but need not base their methods on axioms or formal systems. They would say that you can switch out your foundations and have the same math for all purposes you care about (if you don't care about axioms). While I don't agree with everything there, I think they definitely make a point that's worth thinking about. For example, very few mathematicians would be able to spell out from memory "their basic axioms" (maybe ZFC, category theory, etc., maybe they don't even know or care, or switch depending on context). Now why is that? Their work is so far removed from foundations that they don't have to care. They will rightfully demand that their theorems and ways of reasoning be supported by the axioms. Beyond that, you can tinker and change them all you please. They only need a small part of your foundations to do their work. Crucially, most of them wouldn't "waste" their precious time on e.g. "formalizing that minimal foundation". Maybe one could view foundations as a bunch of programming languages where using the high level features looks indistinguishable and almost noone uses the low-level. I think this intuition strongly suggests that eventually computers will win and all mathematicians will use proof systems (maybe without even knowing how they work under the hood). That is, until maybe the machines surpass their reasoning ability so much that humans are obsolete in that space.

dwheeler 3y ago

If you're interested in formalizing math, check out Metamath: https://us.metamath.org https://us.metamath.org. By itself Metamath doesn't embed any particular set of axioms. The most widely used database (axioms and proven theorems) uses classical logic and set theory, but there's also databases for intuitionistic set theory, new foundations, and higher order logic.

panabee 3y ago
thanks so much. this is extremely useful and could help in training a specialized model for math and logic.

c7b 3y ago

Great read, I was expecting it to bring up the four color theorem, but it was actually an even more interesting debate touching on some modern mathematics. I think it's still worth bringing it up: https://en.m.wikipedia.org/wiki/Four_color_theorem https://en.m.wikipedia.org/wiki/Four_color_theorem In a nutshell, they proved that all maps of contiguous countries can be colored using only four colors by reducing the infinite set of possible maps to a finite one and then having a computer check each case. In the 70's, this wasn't considered a 'real' proof, and it was argued that we can't trust the machine the way we can trust human mathematicians. My first reaction upon hearing about that debate was similar to what probably most HN readers would think, that it's arguably the other way round and we should ideally only trust proofs that had been fully formalized by machines. Glad to see that we're making progress in this direction. Also worth mentioning: apart from Coq that was discussed in the article, there's also the Lean theorem prover that also features some more general programming elements, it's regularly discussed on HN: https://news.ycombinator.com/item?id=36107796 https://news.ycombinator.com/item?id=36107796 https://news.ycombinator.com/item?id=34456573 https://news.ycombinator.com/item?id=34456573

Animats 3y ago
> In the 70's, this wasn't considered a 'real' proof. I ran into that decades ago. We used the original Boyer-Moore theorem prover [1] as part of a program verification system. The system had two provers, the Nelson-Oppen simplifier (the first SAT solver) to automatically handle the easy proofs, and the Boyer-Moore system for the hard ones. To make sure that both had consistent theories, I used the Boyer-Moore prover to prove the "axioms" of the Nelson-Oppen system, especially what are usually called McCarthy's axioms (the ones that use Select and Store) for arrays. The Boyer-Moore system uses a strictly constructive approach to mathematics. It starts from something like Peano arithmetic (there is a number zero, and an operation add 1) and builds up number theory. So I added a concept of arrays, represented as (index, value) tuples in sorted order, and was able to prove the usual "axioms" for arrays as theorems. The machine proofs were long and involved much case analysis.[2] I submitted a paper to JACM in the early 1980s and got back reviews saying that it was just too long and inelegant to be at the fundamentals of computer science. That might not be the case today. A few years back, I put the Boyer-Moore prover on Github, after getting it to work with Gnu Common LISP. So you can still run all this 1980s stuff. It's much faster today. It took about 45 minutes to grind through these proofs on a VAX 11/780 in the early 1980s. Now it takes about a second. The proof log [2] is amusing. It's building up number theory from a very low level, starting by proving that X + 0 = X. Each theorem proved can be used as a lemma by later theorems, so you guide the process by giving it problems to solve in the right order. By line 1900, it's proving that multiplication distributes over addition. Array theory, the new stuff, starts around line 2994. The reason this is so complicated and ugly is that there's no use of axiomatic set theory. Arrays are easy if you have sets. But there are no sets here. Sets don't fit well into this strict constructive theory, because EQUAL means identical. You can't create weaker definitions of equality which say that two sets are equal if they contain the same elements regardless of order, because that introduces a risk of unsoundness. Effort must be put into keeping the tuples of the array representation in ascending order by subscript, which implies much case analysis. Mathematicians hate case analysis. Computers are good at it. [1] https://github.com/John-Nagle/nqthm https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temporaryrulebaseprooflog.txt https://github.com/John-Nagle/pasv/blob/master/src/work/temp...

TechBro8615 3y ago

> “The drive to mechanize proof and proof verification doesn’t strongly motivate most mathematicians as far as I can tell,” he [Michael Harris] said. “I can understand why computer scientists and logicians would be excited, but I think mathematicians are looking for something else.” I'm not a mathematician, but I have at times been able to consider myself a computer scientist. To me, the goal of "mechanizing" and formalizing mathematics seems instinctively recognizable as a worthwhile pursuit, for the same reason it's worth adding tests to an unwieldy legacy codebase: it makes it possible to refactor, to experiment and break things and see what happens. The more we formalize the most fundamental axioms and theorems of mathematics, the more confidently we can alter or remove them and see what happens to the rest of the system. Achieving "100% test coverage" and "instrumentation" of mathematics would allow us to analyze the system under stress. We could fuzz it. We could refactor it. We could even ask an AI to do that for us. As a relative layman, I'm often struck by how many mathematical theorems are dependent on the arbitrary paths we took to develop them. For the same reason, it's a common occurrence that one mathematician discovers an innovation in one branch of mathematics by simply borrowing a common technique from a distantly related branch. Those sorts of analogies and connections between ideas are difficult for humans to spot, and their discovery scales linearly with the number of mathematicians, who might prefer to spend their time discovering truly new ideas rather than repurposing those already existing ideas. But computers, on the other hand, are excellent at spotting these relationships, if given sufficiently formalized definitions of them. So that's why I'd be most excited about formalizing mathematics: how much low-hanging fruit is waiting to be discovered by computers that are just missing the right prompt?

giraj 3y ago
Most mathematicians aren't interested in refactoring their mathematical "codebase", nor experimenting with axioms. They simply want to understand and discover more math. The reasons you state for your interest in formalisation don't appeal to most mathematicians. Concerning analogies and borrowing techniques between fields, this is absolutely something humans are good at and which it is very hard for computers to do. Why do you think otherwise? To take a very simple example, most mathematical objects can be represented in different ways. A mathematician can fluently move between these representations, whereas computers cannot. This is a largely the obstacle for the adoption of proof assistants among mathematicians.

giraj 3y ago

For those interested in formalisation of homotopy type theory, there are several (more or less) active and developed libraries. To mention a few: UniMath (https://github.com/UniMath/UniMath https://github.com/UniMath/UniMath, mentioned in the article) Coq-HoTT (https://github.com/HoTT/Coq-HoTT https://github.com/HoTT/Coq-HoTT) agda-unimath (https://unimath.github.io/agda-unimath/ https://unimath.github.io/agda-unimath/) cubical agda (https://github.com/agda/cubical https://github.com/agda/cubical) All of these are open to contributions, and there are lots of useful basic things that haven't been done and which I think would make excellent semester projects for a cs/math undergrad (for example).

deleted 3y ago

[deleted]

dboreham 3y ago

Odd choice of article title. It appears to be about the well known field: "foundations of mathematics", and is even in a section of the web site named "foundations of mathematics". Meanwhile the word "root" doesn't appear anywhere in the article.

hgsgm 3y ago
And more unfortunately, the "roots" of mathematics always lead to nothing (0).

cubefox 3y ago

(2015) Unfortunately, Voevodsky, the "hero" of this piece, died in 2017.

orlandpm 3y ago

(2015)

b215826 3y ago
Yes, and Voevodsky is no longer alive.

deleted 3y ago

[deleted]