Formalising Mathematics: An Introduction
xenaproject.wordpress.com
Formalising Mathematics: An Introduction
1–10 of 125 posts
Re: Formalising Mathematics: An Introduction
#2I think that something like http://us.metamath.org/index.html has already gone a long way in formalizing math. And this is not the only attempt to formalize math, but it is unique that it uses a very limited amount of syntax and rules, and makes use of a simple (small) proof engine, which makes verifying that the proof engine is correct possible.
Re: Formalising Mathematics: An Introduction
#3I wish these attempts were using constructive mathematics but I understand that that would turn away a lot of mathematicians.
Re: Formalising Mathematics: An Introduction
#4I think that something like http://us.metamath.org/index.html has already gone a long way in formalizing math. And this is not the only attempt to formalize math, but it is unique that it uses a very limited amount of syntax and rules, and makes use of a simple (small) proof engine, which makes verifying that the proof engine is correct possible.
A small proof engine, and maybe a limited amount of rules (depending on the exact technical meaning of 'rules') is a good thing, but I'd say a limited amount of syntax is a bad thing. Mathematicians as a community tend to be happy with—I might even say to prefer—lots of syntax, and, if you want to get a formalisation process really going, layering it with enough syntactic sugar to bring in mathematicians who aren't usually 'formalisers' is going to be essential.
It's also true that there are lots of attempts at formalisation out there; I happen to know about vdash.org , for example, but there are certainly others. I think it's good to have an abundance of formalisations, since no one formalisation style is going to appeal to everyone (for example, as already discussed above, probably the more formalisation-minded mathematicians will have a higher tolerance for minimalism).
Re: Formalising Mathematics: An Introduction
#5I think that something like http://us.metamath.org/index.html has already gone a long way in formalizing math. And this is not the only attempt to formalize math, but it is unique that it uses a very limited amount of syntax and rules, and makes use of a simple (small) proof engine, which makes verifying that the proof engine is correct possible.
Lean allows for third party type checkers. There are relatively small alternative type checkers for Lean (e.g. a scala implementation [1]).
Lean's power lies in its elaborator that breaks down complex tactic-based proofs to a core proof language. This elaboration process can be extended with custom tactics and custom syntax, making it way more powerful than metamath.
[1] https://github.com/gebner/trepplein/tree/master/src/main/sca...
Re: Formalising Mathematics: An Introduction
#6Novak Djokovic Wins Third Straight Australian Open Title
https://snip.ly/8mepd7#https://www.nytimes.com/2021/02/21/sp...
Re: Formalising Mathematics: An Introduction
#7I wish these attempts were using constructive mathematics but I understand that that would turn away a lot of mathematicians.
Just pick a different one! There are definitely formalisation efforts out there that use constructive mathematics; for example Coq is so called after the logic, the calculus of constructions, that it uses (https://en.wikipedia.org/wiki/Calculus_of_constructions).
Re: Formalising Mathematics: An Introduction
#8Novak Djokovic Wins Third Straight Australian Open Title https://snip.ly/8mepd7#https://www.nytimes.com/2021/02/21/sp...
Wrong thread?
Re: Formalising Mathematics: An Introduction
#9I wish these attempts were using constructive mathematics but I understand that that would turn away a lot of mathematicians.
Just pick a different one! There are definitely formalisation efforts out there that use constructive mathematics; for example Coq is so called after the logic, the calculus of constructions, that it uses ( https://en.wikipedia.org/wiki/Calculus_of_constructions ).
Hi! Yes! Just pick a different one! The problem is that constructivists have been formalising mathematics for decades and have not really managed to break through into the mainstream mathematical community with their efforts. The difference with Lean's maths library is that we absolutely reject constructivism, which makes Lean far less suitable for certain kinds of computations but conversely far far better equipped for proving all the theorems in an undergraduate mathematics curriculum and then going on to tackle research level mathematical questions of the kind which most mathematicians recognise as "normal mathematics". My argument (I should say that I am the author of the blog post) is that this resolutely non-classical approach is far more likely to arouse the interest of mainstream mathematicians, who rejected constructivism 100 years ago and have never looked back. I can certainly see a role for constructive mathematics, however I know from experience that most working mathematicians reject it and hence the pragmatic approach is to reject it when formalising if we are to start appealing to the mathematical masses.
Re: Formalising Mathematics: An Introduction
#10I wish these attempts were using constructive mathematics but I understand that that would turn away a lot of mathematicians.
Most are... like Coq, Agda, HoTT, etc.