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

91–100 of 125 posts

Re: Formalising Mathematics: An Introduction

#91

Post by auggierose »

Someone wrote: post #89
auggierose wrote: post #29

Earlier quoted context omitted.

I'd say it is still a pretty constructive answer, as you can run both codes, get two concrete answers, and one of them is guaranteed to be right.

“and one of them is guaranteed to be right.” That’s where opinions will differ. That’s only true if you accept the law of the excluded middle. Mainstream math does, but most constructive math does not.

Yup, I do accept the law of the excluded middle. Unreservedly. From a logical point of view, I cannot really imagine what it would mean NOT to be true.

Yes, Kripke semantics makes sense of constructive logic. Topos theory, too. But I really think of all of these embedded in classical logic, and assuming that the law of excluded middle doesn't hold for general reasoning just doesn't make any kind of sense to me.

Re: Formalising Mathematics: An Introduction

#92

Post by fspeech »

Cybiote wrote: post #86
uyt wrote: post #53

Earlier quoted context omitted.

I played it recently. I spent almost a full day to finish all the worlds and then lost interest afterwards. I think I had expectations that it would be a lot less ... tedious? Like I was hoping it would be mostly automated except needing hints whenever it got stuck. Much like how the flavor text would hint to you (the human) that you needed to use certain theorems for certain levels. Instead, it was so low level that…

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 proofs lemmas often take on distinct flavors because how a human normally proves things may be hard to mechanize. Intead of tools for understanding tactics (granted, these could be useful for tacticians :) we really need tools to help us visualize structure of proofs. If I know how to write a lemma, tactical proof is rarely a blocking issue. Once it is checked the tactics become irrelevant. They were just there to convince the proof checker.

Re: Formalising Mathematics: An Introduction

#93

Post by infogulch »

bsdz wrote: post #55

Last month Kevin Buzzard gave an interesting talk "How do you convince mathematicians a theory prover is worth their time?" about how he became involved with LEAN and some of the proofs he formalised with it: https://youtu.be/8PLrxAfmC_o

During Q&A there was a friendly quarrel about 'mainstream' vs 'constructive' maths. I think there's a funny analogy in here, if you let:

    mainstream proof : constructive proof :: program code : machine code
then Kevin is arguing that the idea of actually compiling his beautiful algorithms into machine code is silly, and that compiling program code in general is rather pointless.

Re: Formalising Mathematics: An Introduction

#94

Post by yoneda »

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…

> but can't typically "find their own way" to the proof of a theorem

That's not what proof assistants like Lean and Coq are about. Sure, they can automate some trivial things, but generally their main utility is that they check your reasoning, not come up with it for you.

Re: Formalising Mathematics: An Introduction

#95

Post by ImprobableTruth »

carapace wrote: post #49

The only major problem (IMO) is that Lean and the others (Coq, Hol, Isabelle, Agda, Idris, etc...) are all pretty hard to read. Check out "Automated Propositional Sequent Proofs in Your Browser with Tau Prolog" for a promising approach: https://www.philipzucker.com/javascript-automated-proving/ It's rendering LaTeX proof trees.

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 quickly see that this just tends to make the proof _less_ readable because they become incredibly bloated.

Re: Formalising Mathematics: An Introduction

#96

Post by [deleted] »

kevinbuzzard wrote: post #15
guerrilla wrote: post #12

Earlier quoted context omitted.

The Four Colour Theorem in Coq seems pretty mainstream I'd say... Also I guess you know that you don't personally have to reject LEM to use Agda or whatever, you just can't do everything in it or at least everything the classical way.

This is a milestone result, and its formalisation taught us many things, for example that the systems are capable of handling long proofs about elementary objects. However finite graph theory is not remotely mainstream mathematics. Take your favourite super-prestigious maths prize, for example the Abel Prize or the Fields Medal. Now look at everyone who has won this prize in the last 10 years. That is the definition…

[deleted]

Re: Formalising Mathematics: An Introduction

#97

Post by jhanschoo »

vcdimension wrote: post #63
auggierose wrote: post #48

Earlier quoted context omitted.

Nope, we are not at cross-purposes. You just don't understand what I am saying. Let's say you need an algorithm for a real-life situation, and you manage to write one down. Ok then, you are good to go, just use it! But ... how do you know that the algorithm you have written down is correct? Now, a constructive mathematician would require you to also provide a constructive proof for your algorithm. A mainstream mathem…

Yes, but if I told IBM that I had a proof that a particular algebraic property or relationship related to homomorphic encryption holds true, I'm sure they would much prefer that it was constructive, rather than non-constructive, because they can produce a usable algorithm from the constructive proof. The point is that by exploring mathematics using only constructive proofs, we are guaranteed to produce (possibly usef…

You probably have no experience with constructive proof checkers, else you wouldn't be missing Auggie's point.

> I'm sure they would much prefer that it was constructive, rather than non-constructive

One point against constructivism is that the proof could be less readable.

> can produce a usable algorithm from the constructive proof

No. Between the automated tactics and inductive propositions constructed to carry all kinds of redundant state helpful in proving your properties, your proof objects won't be anywhere near production level. And constructive proof checkers don't intend that to happen anyway: you pretty much define an efficient function in a DSL, then use a different DSL to prove that the function fulfils the properties. The proof object is pretty much a black box with unclear efficiency that wasn't meant for humans to read.

Re: Formalising Mathematics: An Introduction

#98

Post by uyt »

ahelwer wrote: post #61
uyt wrote: post #53

Earlier quoted context omitted.

I played it recently. I spent almost a full day to finish all the worlds and then lost interest afterwards. I think I had expectations that it would be a lot less ... tedious? Like I was hoping it would be mostly automated except needing hints whenever it got stuck. Much like how the flavor text would hint to you (the human) that you needed to use certain theorems for certain levels. Instead, it was so low level that…

No, I think you have a pretty good grasp of things. In the real world people do use more powerful tactics like ring to skip all the low-level algebraic manipulation (which I personally really enjoyed but can see others finding tedious). Your point about proof readability applies to interactive theorem provers generally. You can see a tradeoff here between Lean/Coq and more "literate" formal proof languages like TLA+,…

The algebra was tedious because for example, the very second thing you prove in the tutorial is that addition is associative. If you were teaching this to humans you would then immediately tell them that you now can omit parentheses because you have an algorithm to re-parenthesize however you want.

But instead, for entire rest of the tutorial, you had to manually rewrite every single parenthesis yourself (with syntax that is pretty unergonomic for doing so too).

I guess I found it a little disappointing that it's not easy to instruct it on how to fill in gaps so you can skip steps the same way you would in a human proof (which would only need a note saying that you're using associativity and parens are omitted thereafter, and any human reader will accept that as valid)

Re: Formalising Mathematics: An Introduction

#99

Post by carapace »

ImprobableTruth wrote: post #95
carapace wrote: post #49

The only major problem (IMO) is that Lean and the others (Coq, Hol, Isabelle, Agda, Idris, etc...) are all pretty hard to read. Check out "Automated Propositional Sequent Proofs in Your Browser with Tau Prolog" for a promising approach: https://www.philipzucker.com/javascript-automated-proving/ It's rendering LaTeX proof trees.

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 intuition as to how the real numbers work. I also have a picture of what the graph of a differentiable function looks like. It’s a wobbly line with no kinks in. This is by no means a perfect picture, but it will do in many cases. ...

Re: Formalising Mathematics: An Introduction

#100

Post by carapace »

nynox wrote: post #56
carapace wrote: post #49

The only major problem (IMO) is that Lean and the others (Coq, Hol, Isabelle, Agda, Idris, etc...) are all pretty hard to read. Check out "Automated Propositional Sequent Proofs in Your Browser with Tau Prolog" for a promising approach: https://www.philipzucker.com/javascript-automated-proving/ It's rendering LaTeX proof trees.

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?
Post reply on HN