4 ms·

I am a mathematician and would love to mechanize my proofs. The issue is that systems like Coq construct proofs in a radically different way than how we were t

by kxyvr 3y ago

I am a mathematician and would love to mechanize my proofs. The issue is that systems like Coq construct proofs in a radically different way than how we were trained. I've struggled with Coq even with a somewhat more than a passing knowledge of the system; I used Coq's underlying language Gallina to write interpreters, which were then processed into OCaml while studying in graduate school. At the same time, I can barely turn out a basic proof in Coq. What would help dramatically for me and others that work in applied math are proofs that cover the material in something like Principles of Mathematical Analysis by Walter Rudin. These are proofs that cover basic real analysis and topics like continuity, differentiation, and integration. It would also help to see basic linear algebra proofs such as that all real symmetric matrices have a real eigendecomposition. Now, these may exist and it's been a couple of years since I've looked. If anyone has a link to them, I'd be extraordinary grateful.

giraj 3y ago
For the math that you mention, I would suggest looking at mathlib (https://github.com/leanprover-community/mathlib https://github.com/leanprover-community/mathlib). I agree that the foundations of Coq are somewhat distanced from the foundations most mathematicians are trained in. Lean/mathlib might be a bit more familiar, not sure. That said, I don't see any obstacles to developing classical real analysis or linear algebra in Coq, once you've gotten used to writing proofs in it. I'm curious, which field of math do you work in? Edit: for example, that symmetric matrices have real eigenvalues is shown here in mathlib: https://leanprover-community.github.io/mathlib_docs/analysis/inner_product_space/spectrum.html https://leanprover-community.github.io/mathlib_docs/analysis...
- kxyvr 3y ago
  Thanks for sending by the mathlib examples. They're not particularly intelligible for me, but it's something to work towards. Generally speaking, I work in the intersection between optimization, differential equations, and control. To that end, there's a variety of foundational results in things like optimization theory that I'd like to see formalized such as optimality conditions, convergence guarantees, and convergence rates. Two questions if you know. One, which theorem prover would you recommend for working toward these kinds of results? Two, is there appetite or a place to publish older, known theorems that have been reworked and validated? And, to be clear, two is not particularly important for me and my career, but it is for many of my colleagues and I'm not sure what to tell them about it.
  - giraj 3y ago
    You're welcome! And likewise, thanks for the interesting reply. I'm afraid I have no knowledge of your field, and no idea whether there are good tools and libraries for formalising the things you want. Maybe ask or have a look around the Proof Assistants StackExchange[1]? There are many CS conferences through which you can publish formalised mathematics. One that comes to mind is ITP[2], but there are lots which are announced on mailing lists like TYPES-announce, coq-club, agda... You could look through previous versions of ITP and check out a few of the papers on formalising mathematics to get a feel for what these publications look like. [1] https://proofassistants.stackexchange.com/ https://proofassistants.stackexchange.com/ [2] https://mizar.uwb.edu.pl/ITP2023/ https://mizar.uwb.edu.pl/ITP2023/
jfoutz 3y ago
I am nothing more than an enthusiastic dabbler, but these have helped me. There are two very different directions 1. the sort of full on proof automation with tactics https://direct.mit.edu/books/oa-monograph/4021/Certified-Programming-with-Dependent-TypesA https://direct.mit.edu/books/oa-monograph/4021/Certified-Pro... Dr. Chlipala builds up understanding of the "crush" tactic, which more or less lets you specify an inductive hypothesis, and that tactic fiddles around with identifying the base case, and expanding enough to generate the n+1 step. Along the way, you get exposure to using Gallina to write your own tactics. it's neat, from a programmer point of view, because you can automate away the boring parts. There is pretty good discussion of debugging tactics, which might provide a path to transforming machine proofs into something a bit more comprehensible. at the very least, you can recover the application of axioms and such that did the transformation. The other direction, that has been much more enlightening for me (the amateur hobbyist) was agda and Jesper Cockx's tutorial- https://github.com/jespercockx/agda-lecture-notes/blob/master/agda.pdf https://github.com/jespercockx/agda-lecture-notes/blob/maste... he builds up all of the notation from, well, nothing. for example, you get refl, and then build up -- symmetry of equality sym : {A : Set} {x y : A} → x ≡ y → y ≡ x sym refl = refl -- transitivity of equality trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z (54) trans refl refl = refl -- congruence of equality cong : {A B : Set} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y cong f refl = refl along with the syntax that comes with the agda std lib. agda is different, but you can still extract to Haskell (and allegedly javascript for node, but that was a little flakey for me and might go away in a future release). less useful for your goals, much more programming oriented - https://plfa.github.io https://plfa.github.io is pretty good, and worth mentioning as a reference.
- kxyvr 3y ago
  I'm slow on replies, but thanks for the references. I'll have a look.
skissane 3y ago
Is the problem that human mathematicians have decided that classical logic + ZF(C) is the best framework for them–but it isn’t the best framework for computers? Which raises an interesting philosophical question - do contemporary mathematicians mostly do things one way rather than another (i.e. classical logic instead of intuitionistic/paraconsistent/etc logic, ZF(C) set theory instead of alternative set theories or type theory or whatever, classical analysis instead of non-standard analysis, and so on) - because they’ve settled upon the inherently superior (easier, more productive) way of doing things - or is that just an accident of history? Could it be that in some alternative timeline or parallel universe out there, mathematics took some different forks in the road, and the mathematical mainstream ended up looking very different from how it does here?
- TechBro8615 3y ago
  I find these "fork in the road" questions endlessly fascinating, and that's exactly what I was getting at with my comment about the motivation for formalizing mathematics. And it doesn't just apply to math, but the whole "tech tree" of human history. How many seemingly arbitrary choices led us down a path that unknowingly diverged from some alternative future? Last time I commented about this [0], I made some guy irrationally angry as he told me I sounded like I was 19 years old. And in an earlier comment [1], another guy took extreme offense to my questioning of the statement "with enough marbles, the discrete distribution behaves like a continuous distribution." It seems there is some high priesthood of mathematics and physics that doesn't like when you ask these sorts of questions. [0] https://news.ycombinator.com/item?id=35018407 https://news.ycombinator.com/item?id=35018407 [1] https://news.ycombinator.com/item?id=35201603 https://news.ycombinator.com/item?id=35201603
  - skissane 3y ago
    > Last time I commented about this [0], I made some guy irrationally angry as he told me I sounded like I was 19 years old If people make comments like that, flag them and email dang (hn@ycombinator.com) and he’ll do something about them > It seems there is some high priesthood of mathematics and physics that doesn't like when you ask these sorts of questions In my personal experience, most professional mathematicians and physicists are open to questioning the foundations of their discipline, and deal charitably with doubters (even those who are coming from a place of misunderstanding). I suspect most of the “high priests” you speak of aren’t actually professionals at all, just Internet randoms who (at best) know only slightly more than you do, and who know very little about the norms of civil dialogue

by kxyvr 3y ago

giraj 3y ago

For the math that you mention, I would suggest looking at mathlib (https://github.com/leanprover-community/mathlib https://github.com/leanprover-community/mathlib). I agree that the foundations of Coq are somewhat distanced from the foundations most mathematicians are trained in. Lean/mathlib might be a bit more familiar, not sure. That said, I don't see any obstacles to developing classical real analysis or linear algebra in Coq, once you've gotten used to writing proofs in it. I'm curious, which field of math do you work in? Edit: for example, that symmetric matrices have real eigenvalues is shown here in mathlib: https://leanprover-community.github.io/mathlib_docs/analysis/inner_product_space/spectrum.html https://leanprover-community.github.io/mathlib_docs/analysis...

kxyvr 3y ago
Thanks for sending by the mathlib examples. They're not particularly intelligible for me, but it's something to work towards. Generally speaking, I work in the intersection between optimization, differential equations, and control. To that end, there's a variety of foundational results in things like optimization theory that I'd like to see formalized such as optimality conditions, convergence guarantees, and convergence rates. Two questions if you know. One, which theorem prover would you recommend for working toward these kinds of results? Two, is there appetite or a place to publish older, known theorems that have been reworked and validated? And, to be clear, two is not particularly important for me and my career, but it is for many of my colleagues and I'm not sure what to tell them about it.
- giraj 3y ago
  You're welcome! And likewise, thanks for the interesting reply. I'm afraid I have no knowledge of your field, and no idea whether there are good tools and libraries for formalising the things you want. Maybe ask or have a look around the Proof Assistants StackExchange[1]? There are many CS conferences through which you can publish formalised mathematics. One that comes to mind is ITP[2], but there are lots which are announced on mailing lists like TYPES-announce, coq-club, agda... You could look through previous versions of ITP and check out a few of the papers on formalising mathematics to get a feel for what these publications look like. [1] https://proofassistants.stackexchange.com/ https://proofassistants.stackexchange.com/ [2] https://mizar.uwb.edu.pl/ITP2023/ https://mizar.uwb.edu.pl/ITP2023/

jfoutz 3y ago

I am nothing more than an enthusiastic dabbler, but these have helped me. There are two very different directions 1. the sort of full on proof automation with tactics https://direct.mit.edu/books/oa-monograph/4021/Certified-Programming-with-Dependent-TypesA https://direct.mit.edu/books/oa-monograph/4021/Certified-Pro... Dr. Chlipala builds up understanding of the "crush" tactic, which more or less lets you specify an inductive hypothesis, and that tactic fiddles around with identifying the base case, and expanding enough to generate the n+1 step. Along the way, you get exposure to using Gallina to write your own tactics. it's neat, from a programmer point of view, because you can automate away the boring parts. There is pretty good discussion of debugging tactics, which might provide a path to transforming machine proofs into something a bit more comprehensible. at the very least, you can recover the application of axioms and such that did the transformation. The other direction, that has been much more enlightening for me (the amateur hobbyist) was agda and Jesper Cockx's tutorial- https://github.com/jespercockx/agda-lecture-notes/blob/master/agda.pdf https://github.com/jespercockx/agda-lecture-notes/blob/maste... he builds up all of the notation from, well, nothing. for example, you get refl, and then build up -- symmetry of equality sym : {A : Set} {x y : A} → x ≡ y → y ≡ x sym refl = refl -- transitivity of equality trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z (54) trans refl refl = refl -- congruence of equality cong : {A B : Set} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y cong f refl = refl along with the syntax that comes with the agda std lib. agda is different, but you can still extract to Haskell (and allegedly javascript for node, but that was a little flakey for me and might go away in a future release). less useful for your goals, much more programming oriented - https://plfa.github.io https://plfa.github.io is pretty good, and worth mentioning as a reference.

kxyvr 3y ago
I'm slow on replies, but thanks for the references. I'll have a look.

skissane 3y ago

Is the problem that human mathematicians have decided that classical logic + ZF(C) is the best framework for them–but it isn’t the best framework for computers? Which raises an interesting philosophical question - do contemporary mathematicians mostly do things one way rather than another (i.e. classical logic instead of intuitionistic/paraconsistent/etc logic, ZF(C) set theory instead of alternative set theories or type theory or whatever, classical analysis instead of non-standard analysis, and so on) - because they’ve settled upon the inherently superior (easier, more productive) way of doing things - or is that just an accident of history? Could it be that in some alternative timeline or parallel universe out there, mathematics took some different forks in the road, and the mathematical mainstream ended up looking very different from how it does here?

TechBro8615 3y ago
I find these "fork in the road" questions endlessly fascinating, and that's exactly what I was getting at with my comment about the motivation for formalizing mathematics. And it doesn't just apply to math, but the whole "tech tree" of human history. How many seemingly arbitrary choices led us down a path that unknowingly diverged from some alternative future? Last time I commented about this [0], I made some guy irrationally angry as he told me I sounded like I was 19 years old. And in an earlier comment [1], another guy took extreme offense to my questioning of the statement "with enough marbles, the discrete distribution behaves like a continuous distribution." It seems there is some high priesthood of mathematics and physics that doesn't like when you ask these sorts of questions. [0] https://news.ycombinator.com/item?id=35018407 https://news.ycombinator.com/item?id=35018407 [1] https://news.ycombinator.com/item?id=35201603 https://news.ycombinator.com/item?id=35201603
- skissane 3y ago
  > Last time I commented about this [0], I made some guy irrationally angry as he told me I sounded like I was 19 years old If people make comments like that, flag them and email dang (hn@ycombinator.com) and he’ll do something about them > It seems there is some high priesthood of mathematics and physics that doesn't like when you ask these sorts of questions In my personal experience, most professional mathematicians and physicists are open to questioning the foundations of their discipline, and deal charitably with doubters (even those who are coming from a place of misunderstanding). I suspect most of the “high priests” you speak of aren’t actually professionals at all, just Internet randoms who (at best) know only slightly more than you do, and who know very little about the norms of civil dialogue