Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Formalising Mathematics: An Introduction

xenaproject.wordpress.com

Post reply on HN
Print view View original

101–110 of 125 posts

Re: Formalising Mathematics: An Introduction

#101

Post by _ouml_ »

dash2 wrote: post #66

Outsider's question: is it likely that projects like Lean and Coq will ever feed into stuff that applied researchers find useful? By applied researchers I don't mean "applied mathematicians" but scientists who use maths in their field. As an economist, I sometimes want to prove things that a real mathematician could do in their sleep. There's Mathematica and friends, but they have their limitations, i.e. they can do…

Yes, these systems are being used to formally verify implementations of cryptographic protocols, or implementations of numerical algorithms, for example.

Note that there are two distinct components that interact: (i) verification of proofs and (ii) automation of finding the proofs. The latter is very much an active field of research, but so far isn't of the level that it will prove most of your theorems for you.

Re: Formalising Mathematics: An Introduction

#102

Post by _ouml_ »

317070 wrote: post #84

> However, AI works best with a database — and those databases are not yet there. They do, but I would tell you that if that is your main motivation to create those databases, don't do it. The AI might spend milliseconds on work that takes man-years to compile, but get stuck on absolutely tiny issues of details it can't grok and which you can quickly explain. If AI is the goal, I would propose to discuss with AI-rese…

There is a very active community around Lean ranging from mathematicians with no clue about computers to AI researchers trying to improve the automation. These AI researchers have explicitly said that bigger training sets will be very helpful. But like the sibling comment says, AI is not the main point.

Re: Formalising Mathematics: An Introduction

#103

Post by Cybiote »

fspeech wrote: post #92
Cybiote wrote: post #86

Earlier quoted context omitted.

I originally intended to write what follows as its own comment but, although I used Coq instead of Lean and worked through a different set of exercises, your criticisms so closely mirrored mine, I decided to reply here instead, and point out promising paths to solutions. I too felt it a waste of time to prove things that were clearly "obvious". Of course, in math, some of the most frightening words to encounter are "…

Actually there isn't much to understanding the tactics unless you want to use them similarly, just like you wouldn't bother looking into what "auto" has done. For understanding math it is a lot more important to understand the lemmas and why they are structured certain way, akin to understanding the API of programs. We can think of theorems as math's public API and lemmas the internal API for devs. In machine checked…

All what you say makes sense, especially as one becomes more comfortable with tactics but I maintain formal proofs are a lot harder to parse than regular math proofs. Having to write for both machine and human distorts a proof's natural flow and reading them often feels like trying to understand partially commented code by executing it in your head.

Well commented proofs are good to communicate intent but if you also want to be able to reproduce a similar proof, it's often useful to understand why tactics were deployed as they were. The existence of the wonderful https://plv.csail.mit.edu/blog/alectryon.html bears out the importance and utility of this.

> For understanding math

My contention, which I believe is shared by the article, is that this understanding is often flimsier than most think, particularly as one leaves well trafficked areas held together by tacit knowledge and knowledge of multiple reinforcing paths shared within communities with relevant expertise. However, even that is insufficient for less used lemmas.

This structuring of knowledge will be useful for mathematics education and research both, especially from the perspective of an individual human trying to safely use results of proofs.

> we really need tools to help us visualize structure of proofs

The output proof is a program, so the problem of visualizing proofs is much the same as visualizing programs and visual programming, sharing the same hurdles. Perhaps friendlier naming and formatting of output code in proof tools will be useful. I believe something more useful would be queryable visualizations of how theorems and lemmas connect and relate to each other.

Re: Formalising Mathematics: An Introduction

#104

Post by edanm »

btilly wrote: post #88

If anyone wants of a concrete reason to formalize mathematics, consider this. The classification of finite simple groups is a major result in mathematics that is a foundation for many others. See https://en.wikipedia.org/wiki/Classification_of_finite_simpl... for more. However at the time the proof was finishing, people were leaving the field, and the very people who proved it did not feel that their results were che…

> I maintain that no amount of human verification and re-verification will result in my being as confident of this result as I am about most mathematical results that I know. The only way to actually make this into something we should be confident of is to translate the existing proofs to something computer checkable.

Or to indeed find that simpler proof, I suppose?

(Not disagreeing with anything you're saying, just checking - it's a fascinating story that I didn't know about this topic)

Re: Formalising Mathematics: An Introduction

#105

Post by Someone »

ithinkso wrote: post #87
stacksemantics wrote: post #81

Earlier quoted context omitted.

Constructive mathematics does not affirm excluded middle. That's distinct from rejecting it.

What do you mean? (sorry, english is not my first language). The way I understand it is that if you have the law of excluded middle you cannot discard 'non-constructive' proofs as invalid since they follow straight from the axioms.

“Not affirm” means they don’t take it as an axiom (“we don’t take this to be obviously true”)

“reject” would mean that if, given their set of axioms, it could be proven, they would try and tweak their axioms in order to make it unprovable or provably false in their system (“we think this cannot and should not be true”)

So, “not reject” means they would happily use it in their proofs, if it could be proven from their set of axioms (“interesting. That gives us a powerful tool to do proofs”)

Re: Formalising Mathematics: An Introduction

#106

Post by stacksemantics »

ithinkso wrote: post #87
stacksemantics wrote: post #81

Earlier quoted context omitted.

Constructive mathematics does not affirm excluded middle. That's distinct from rejecting it.

What do you mean? (sorry, english is not my first language). The way I understand it is that if you have the law of excluded middle you cannot discard 'non-constructive' proofs as invalid since they follow straight from the axioms.

Constructive mathematicians do not assert that excluded middle is true since there is no constructive proof of (P not P). Nor do they assert that it is false, since that statement, (not (P or not P)), is constructively refutable i.e. there is a constructive proof of (not not (P or not P)). So there are no instances in constructive mathematics where excluded middle is false. But there are constructive settings where excluded middle holds, e.g. Boolean topoi, but you have to prove excluded middle is validated.

So we can't claim constructive mathematicians reject excluded middle, since they reject the rejection of excluded middle. I admit this will be confusing for people used to classical logic at first, even those for whom English is their native language.

> The way I understand it is that if you have the law of excluded middle you cannot discard 'non-constructive' proofs as invalid since they follow straight from the axioms.

This is accurate, my above point is just a pedantic one about semantics.

Re: Formalising Mathematics: An Introduction

#107

Post by schoen »

edanm wrote: post #104
btilly wrote: post #88

If anyone wants of a concrete reason to formalize mathematics, consider this. The classification of finite simple groups is a major result in mathematics that is a foundation for many others. See https://en.wikipedia.org/wiki/Classification_of_finite_simpl... for more. However at the time the proof was finishing, people were leaving the field, and the very people who proved it did not feel that their results were che…

> I maintain that no amount of human verification and re-verification will result in my being as confident of this result as I am about most mathematical results that I know. The only way to actually make this into something we should be confident of is to translate the existing proofs to something computer checkable. Or to indeed find that simpler proof, I suppose? (Not disagreeing with anything you're saying, just…

I don't understand this area well at all, but I know the existing classification of finite simple groups is very long and detailed.

Wikipedia says

> The proof consists of tens of thousands of pages in several hundred journal articles

and that the second-generation simplified version might possibly run to only 5,000 pages.

5,000 pages of math is easier to understand and/or believe in than tens of thousands of pages, but it's still a pretty daunting amount even for specialists.

Re: Formalising Mathematics: An Introduction

#108

Post by fspeech »

Cybiote wrote: post #103
fspeech wrote: post #92

Earlier quoted context omitted.

Actually there isn't much to understanding the tactics unless you want to use them similarly, just like you wouldn't bother looking into what "auto" has done. For understanding math it is a lot more important to understand the lemmas and why they are structured certain way, akin to understanding the API of programs. We can think of theorems as math's public API and lemmas the internal API for devs. In machine checked…

All what you say makes sense, especially as one becomes more comfortable with tactics but I maintain formal proofs are a lot harder to parse than regular math proofs. Having to write for both machine and human distorts a proof's natural flow and reading them often feels like trying to understand partially commented code by executing it in your head. Well commented proofs are good to communicate intent but if you also…

The flimsiness of one's understanding tends to manifest as false "lemmas", which can't really be proved because one forgot certain conditions that are typically implicit with human understanding but must be made explicit formally. However if a proof can be completed then it's solid by definition. I would contend when a proof becomes hard to understand instead of documenting tactics one should break up the proof into more lemmas or create more subgoals; preferrably all tactics are "auto". It's nice that the tool you referred to is general and can be used to document any prospect of proof but being based on a markup language it is mostly static. When Gonthier mechanized Feit-Thompson Odd Order Theorem, he had very large graphs showing the relationship of the lemmas. Unfortunately those were also static as I remember and only really comprehensible to the experts. It would be nice to have interactive versions that can aid an average reader on comprehending and exploring the overall relationships. Such a tool is also sorely missing for understanding large code bases. The two are really two sides of the same coin through Curry-Howard. The good thing is a tool that lets users efficiently navigate structures can be done without extra effort of the proof writer (of course documenting intention is always important).

Re: Formalising Mathematics: An Introduction

#109

Post by nynox »

carapace wrote: post #100
nynox wrote: post #56

Earlier quoted context omitted.

Following this proof tree idea, this recent paper https://arxiv.org/abs/2102.03044 suggests to think of proofs of theorems as large trees, a tiny subset of which needs to be made explicit to convey the confidence the rest could be written out (if ever needed).

Does that presuppose that it's computationally expensive to verify proofs? If so, isn't that kind of unrealistic?

Verifying fully formalized proofs is cheap. What is expensive is to produce such formalized proofs. More precisely, to formalize a proof written in a typical math paper is extremely time-consuming and not so informative (that's why it's almost never done in practice).

Re: Formalising Mathematics: An Introduction

#110

Post by robinzfc »

carapace wrote: post #99
ImprobableTruth wrote: post #95

Earlier quoted context omitted.

Proof trees just become unmanageable for anything but trivial example and not only that, their biggest benefit - knowing which rule is applied, doesn't get you much for a dependent type system. Not to mention that any format that isn't just strictly text is probably doomed to fail from the start. If you want essentially a text version of proof trees, just write fully annotated terms for your proofs. I think you'll qu…

Hmm... If not proof trees, what? > Not to mention that any format that isn't just strictly text is probably doomed to fail from the start. LaTeX is text. (I'm not being snarky.) - - - - The key might be in formalizing the subjective processes like what was described starting here: > Mathematicians think in pictures > I have a picture of the real numbers in my head. It’s a straight line. This picture provides a great…

> If not proof trees, what?

Just make the proof language similar to the standard mathematics language and possibly process it with a presentation layer that makes it even better. The examples start from Mizar [1] (since 1973), IsarMathLib [2] (disclaimer: my project), Naproche-SAD [3] (bundled with Isabelle recently) [1] http://mizar.org/ [2] https://isarmathlib.org/ [3] http://ceur-ws.org/Vol-2634/FMM4.pdf

Post reply on HN