5 ms·

This is going to be an exciting area. I spent some time previously playing with Coq. It's very powerful, but even proving the simplest undergraduate maths stat

This is going to be an exciting area. I spent some time previously playing with Coq. It's very powerful, but even proving the simplest undergraduate maths statements (say, about group theory) can prove very challenging. I believe that part of this is that Coq uses different mathematical foundations than traditional mathematics, which mostly uses set theory (ZFC, although most people don't care about the specifics). So it can be hard or unnatural to express something like "subgroup". I don't know if Lean fares better in that respect. Coq documentation is also IMHO almost impossible to understand unless you're already very deeply knowledgeable about the system. We will probably still need some more iterations, to get more user friendly assistants with better documentation and to get adequate teaching resources etc.

raphlinus 5y ago
Lean's foundations are similar to Coq. I think the ergonomics are a bit better. Most activity in proof systems is based in type theory these days, but set theoretical systems do exist, of which Metamath is the most mature. That said, Metamath is seriously lacking in automation, so there is an element of tedium involved. That's not because of any fundamental limitations, but I think mostly because people working in the space are more motivated to do things aligned with programming language theory. There was also a talk by John Harrison a few years ago proposing a fusion of HOL and set theory, but I'm not sure there's been much motion since then. I believe a fully featured proof assistant based in set theory would be a great contribution. [1]: http://aitp-conference.org/2018/slides/JH.pdf http://aitp-conference.org/2018/slides/JH.pdf
- robinzfc 5y ago
  It depends on what you mean by "fully featured" but Isabelle supports ZF logic [1] and also you can do ZFC in Isabelle/HOL [2]. And, of course there is Mizar [3]. [1] https://isabelle.in.tum.de/dist/library/ZF/ZF/index.html https://isabelle.in.tum.de/dist/library/ZF/ZF/index.html [2] https://www.isa-afp.org/entries/ZFC_in_HOL.html https://www.isa-afp.org/entries/ZFC_in_HOL.html [3] http://mizar.org/ http://mizar.org/
Ericson2314 5y ago
You don't need subgroups, you just need injective homomorphisms.
- Jweb_Guru 5y ago
  That's a nice idea but it tends to fall flat when you can't actually construct an explicit function exhibiting the homomorphism in question (which does happen from time to time). A lot of equivalences in areas like group theory only hold classically.
  - Ericson2314 5y ago
    Your concerns make sense in general, but I have hard time understanding them for would-be subgroups. I would think the "explicit function" would be the easy part. The hard pat is annoyance of finding a "syntactic" representation of the subgroup and proving it's a group (closed) in its own right. In any event, Lean's reputation is that it goes the extra mile for "regular" mathematicians. It probably has something nicer for this just like it does for quotiented types.
    - Jweb_Guru 5y ago
      Nope, proving something is a group doesn't usually run into foundational concerns (at least if you use setoid equality). But finding a function exhibiting a homomorphism can unless you use a functional relation instead (but then you lose most of the nice benefits of using this version of the definition in the first place).
zozbot234 5y ago
ZFC was only ever developed as a proof of concept, not as a practical foundation for formal math. Structural set theories, type theories or category-based foundations are actually a lot easier to work with, and otherwise quite equivalent in power.
- Tainnor 5y ago
  This is missing the point. Modern mathematics textbooks, especially undergratuate ones, are written with set theoretic foundations. It requires a lot of effort to reformulate all of mathematics into equivalent formulations. That makes it harder to get buy-in from many working mathematicians, and it also makes the subject less approachable for, say, undergraduates.
  - zozbot234 5y ago
    Modern math textbooks are based on naïve set theory, which can be quite feasibly modeled, even by structural foundations. It might require some effort at the lowest layer of formalization, but even then only as a one-time thing that's not going to impact the project as a whole.
    - Tainnor 5y ago
      That may very well be the case, but to a person starting out right now, those foundations seem to be lacking right now (or at least are not easily discoverable).
  - creata 5y ago
    > Modern mathematics textbooks, especially undergratuate ones, are written with set theoretic foundations. Yes, but only the foundations. A math undergrad doesn't actually care whether an ordered pair (a, b) is encoded as {{a},{a,b}} or as an instance of the product type, and they don't care whether the natural number 2 is encoded as the set {{},{{}}} or as a value S(S(Z)) of the inductive type of the natural numbers. Although if pressured to choose, I bet they'd prefer the latter, since it gets a lot closer to how everyone thinks of "ordered pairs" and "natural numbers". Since mathematicians always work with higher-level abstractions anyway, I don't think the fact that the very lowest layer of these abstractions is set theory actually gets in the way of formalization efforts.
deadbeef57 5y ago
In my experience, the difficulty is very rarely the transition from set theory to type theory. I find this almost transparent in practice. The issue is rather that you need to deal with edge cases that are usually swept under the rug, or that you need to spend a full page working out the details of a proof that everyone recognizes as obvious. It would be great if computers could give even more assistance with these tedious parts of formalization, and I'm very glad that people are working hard on realizing this.
- ganzuul 5y ago
  Kurt Gödel with a bat in dark alleyway of obviousness haunts my dreams.
- chriswarbo 5y ago
  One area I've been playing with is "theory exploration", which takes a set of definitions and produces lemmas that are 'interesting' (i.e. irreducible, via some scheme like Knuth-Bendix rewriting). (Thanks to Curry-Howard, we can also view this as generating test suites/specifications for software libraries!) Notable tools include Hipster, IsaScheme, IsaCoSy, QuickSpec and Speculate.
ixaxaar 5y ago
Hey type hacking is hard. Agda is kinda easier for someone who knows haskell, but hard nonetheless.
kmill 5y ago
Here's the definition of a subgroup in Lean's mathlib: https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html#subgroup https://leanprover-community.github.io/mathlib_docs/group_th... Given a group G, there is a type `subgroup G` of subgroups of G, and a subgroup is a structure consisting of a set of elements of G along with some proofs that it has the identity, it's closed under multiplication, and it's closed under taking inverses. Lean has a coercion facility using typeclasses, and there is a typeclass instance that will use the subgroup's set coerced to a type when the subgroup is used in a place that expects a type. This coerced type has a group typeclass instance, so a subgroup "is" a group. The big complexity in all of this doesn't seem to be ZFC vs type theory, but rather how do you implement a mathematician's use of synecdoche and implicit coercions. Synecdoche is the figure of speech where you refer to a thing by its parts or vice versa -- for example, "let G be a group" and then using G as if it were a set, even though a group consists of a set, a binary operation on the set, a choice of identity element, and a few axioms that must hold. Mathlib uses typeclasses to implement the synecdoche -- a type is a group if there is a typeclass instance that provides the rest of the structure. As I understand it, Coq's Mathematical Components library uses structures and unification hints instead (though I've failed to understand how it works exactly), but I have heard that they can be very fiddly to get right. I think you'd have to find solutions to these same problems no matter the foundations. At least with types, there's enough information lying around that, for example, group structures can be automatically synthesized by the typeclass resolution system in many common situations.

raphlinus 5y ago

Lean's foundations are similar to Coq. I think the ergonomics are a bit better. Most activity in proof systems is based in type theory these days, but set theoretical systems do exist, of which Metamath is the most mature. That said, Metamath is seriously lacking in automation, so there is an element of tedium involved. That's not because of any fundamental limitations, but I think mostly because people working in the space are more motivated to do things aligned with programming language theory. There was also a talk by John Harrison a few years ago proposing a fusion of HOL and set theory, but I'm not sure there's been much motion since then. I believe a fully featured proof assistant based in set theory would be a great contribution. [1]: http://aitp-conference.org/2018/slides/JH.pdf http://aitp-conference.org/2018/slides/JH.pdf

robinzfc 5y ago
It depends on what you mean by "fully featured" but Isabelle supports ZF logic [1] and also you can do ZFC in Isabelle/HOL [2]. And, of course there is Mizar [3]. [1] https://isabelle.in.tum.de/dist/library/ZF/ZF/index.html https://isabelle.in.tum.de/dist/library/ZF/ZF/index.html [2] https://www.isa-afp.org/entries/ZFC_in_HOL.html https://www.isa-afp.org/entries/ZFC_in_HOL.html [3] http://mizar.org/ http://mizar.org/

Ericson2314 5y ago

You don't need subgroups, you just need injective homomorphisms.

Jweb_Guru 5y ago
That's a nice idea but it tends to fall flat when you can't actually construct an explicit function exhibiting the homomorphism in question (which does happen from time to time). A lot of equivalences in areas like group theory only hold classically.
- Ericson2314 5y ago
  Your concerns make sense in general, but I have hard time understanding them for would-be subgroups. I would think the "explicit function" would be the easy part. The hard pat is annoyance of finding a "syntactic" representation of the subgroup and proving it's a group (closed) in its own right. In any event, Lean's reputation is that it goes the extra mile for "regular" mathematicians. It probably has something nicer for this just like it does for quotiented types.
  - Jweb_Guru 5y ago
    Nope, proving something is a group doesn't usually run into foundational concerns (at least if you use setoid equality). But finding a function exhibiting a homomorphism can unless you use a functional relation instead (but then you lose most of the nice benefits of using this version of the definition in the first place).

zozbot234 5y ago

ZFC was only ever developed as a proof of concept, not as a practical foundation for formal math. Structural set theories, type theories or category-based foundations are actually a lot easier to work with, and otherwise quite equivalent in power.

Tainnor 5y ago
This is missing the point. Modern mathematics textbooks, especially undergratuate ones, are written with set theoretic foundations. It requires a lot of effort to reformulate all of mathematics into equivalent formulations. That makes it harder to get buy-in from many working mathematicians, and it also makes the subject less approachable for, say, undergraduates.
- zozbot234 5y ago
  Modern math textbooks are based on naïve set theory, which can be quite feasibly modeled, even by structural foundations. It might require some effort at the lowest layer of formalization, but even then only as a one-time thing that's not going to impact the project as a whole.
  - Tainnor 5y ago
    That may very well be the case, but to a person starting out right now, those foundations seem to be lacking right now (or at least are not easily discoverable).
- creata 5y ago
  > Modern mathematics textbooks, especially undergratuate ones, are written with set theoretic foundations. Yes, but only the foundations. A math undergrad doesn't actually care whether an ordered pair (a, b) is encoded as {{a},{a,b}} or as an instance of the product type, and they don't care whether the natural number 2 is encoded as the set {{},{{}}} or as a value S(S(Z)) of the inductive type of the natural numbers. Although if pressured to choose, I bet they'd prefer the latter, since it gets a lot closer to how everyone thinks of "ordered pairs" and "natural numbers". Since mathematicians always work with higher-level abstractions anyway, I don't think the fact that the very lowest layer of these abstractions is set theory actually gets in the way of formalization efforts.

deadbeef57 5y ago

In my experience, the difficulty is very rarely the transition from set theory to type theory. I find this almost transparent in practice. The issue is rather that you need to deal with edge cases that are usually swept under the rug, or that you need to spend a full page working out the details of a proof that everyone recognizes as obvious. It would be great if computers could give even more assistance with these tedious parts of formalization, and I'm very glad that people are working hard on realizing this.

ganzuul 5y ago
Kurt Gödel with a bat in dark alleyway of obviousness haunts my dreams.
chriswarbo 5y ago
One area I've been playing with is "theory exploration", which takes a set of definitions and produces lemmas that are 'interesting' (i.e. irreducible, via some scheme like Knuth-Bendix rewriting). (Thanks to Curry-Howard, we can also view this as generating test suites/specifications for software libraries!) Notable tools include Hipster, IsaScheme, IsaCoSy, QuickSpec and Speculate.

ixaxaar 5y ago

Hey type hacking is hard. Agda is kinda easier for someone who knows haskell, but hard nonetheless.

kmill 5y ago

Here's the definition of a subgroup in Lean's mathlib: https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html#subgroup https://leanprover-community.github.io/mathlib_docs/group_th... Given a group G, there is a type `subgroup G` of subgroups of G, and a subgroup is a structure consisting of a set of elements of G along with some proofs that it has the identity, it's closed under multiplication, and it's closed under taking inverses. Lean has a coercion facility using typeclasses, and there is a typeclass instance that will use the subgroup's set coerced to a type when the subgroup is used in a place that expects a type. This coerced type has a group typeclass instance, so a subgroup "is" a group. The big complexity in all of this doesn't seem to be ZFC vs type theory, but rather how do you implement a mathematician's use of synecdoche and implicit coercions. Synecdoche is the figure of speech where you refer to a thing by its parts or vice versa -- for example, "let G be a group" and then using G as if it were a set, even though a group consists of a set, a binary operation on the set, a choice of identity element, and a few axioms that must hold. Mathlib uses typeclasses to implement the synecdoche -- a type is a group if there is a typeclass instance that provides the rest of the structure. As I understand it, Coq's Mathematical Components library uses structures and unification hints instead (though I've failed to understand how it works exactly), but I have heard that they can be very fiddly to get right. I think you'd have to find solutions to these same problems no matter the foundations. At least with types, there's enough information lying around that, for example, group structures can be automatically synthesized by the typeclass resolution system in many common situations.