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

61–70 of 125 posts

Re: Formalising Mathematics: An Introduction

#61

Post by ahelwer »

uyt wrote: post #53
schoen wrote: post #25

A game to try this out (by Kevin Buzzard, who is participating in this thread and is also the author of this blog post). https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam... I loved it and have been trying to make some subsequent levels about divisibility.

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+, which has a prover called TLAPS (TLA+ Proof System). TLA+ proofs are written in a hierarchical style Lamport proposed in his paper How to Write a 21st Century Proof[0], and are readable by themselves. The BIG BIG tradeoff here is that when you're writing the proof in TLA+, it's very difficult to know what the prover is "thinking" and why it is stuck. Whereas with interactive provers you know exactly what the prover is "thinking" - the proof consists solely of instructions to manipulate those thoughts which you see on screen at all times! So at this time it seems there's a tradeoff between ease of writing a formal proof and ease of reading a formal proof.

[0] https://www.microsoft.com/en-us/research/publication/write-2...

Re: Formalising Mathematics: An Introduction

#62

Post by auggierose »

kmill wrote: post #52
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.

A way to think about whether something is constructive is that everything is decidable, in the sense that there is some procedure that will give you the answer in finite time. In Kevin's example where you have two programs, one which depends on the Riemann hypothesis being true and the other which depends on it being false, is that you can't just execute the programs -- they might have undefined behavior since they d…

Yeah, I really was joking.

Re: Formalising Mathematics: An Introduction

#63

Post by vcdimension »

auggierose wrote: post #48
vcdimension wrote: post #47

Earlier quoted context omitted.

I think we're at cross-purposes; I am talking about mathematics for the purpose of real-life useful applications (e.g. cryptography, data analysis, etc), in which case you need algorithms.

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 useful) algorithms. If you already have an algorithm, and can prove it works non-constructively then fine, but a collection of N non-constructive proofs is not nearly so useful for real-life applications as a collection of N constructive ones.

Re: Formalising Mathematics: An Introduction

#64

Post by spekcular »

QuesnayJr wrote: post #46
spekcular wrote: post #40

Earlier quoted context omitted.

I think the (implicit) charge that the editors of top journals are keeping good papers out for snobbish reasons is mostly unfounded. I don't deny that their tastes shape what gets published, of course. But in most circumstances, they are not subject matter experts, and the first step of evaluating any paper is that is not an obvious desk-reject (for poor writing, crankery, etc.) is to send it to a group of relevant e…

There was a notorious case that a paper by Wehring solving the largest outstanding question in lattice theory was rejected by JAMS despite glowing referee reports (and being pretty short). So it's pretty much an example of editors arbitrarily killing a paper. (It appeared in Advances in Mathematics.) You can see a letter to the editor of the Bulletin about it. Look at the affiliations of the people protesting the dec…

I don't really see a problem with this decision, though I am sympathetic to Wehrung. As the editors note, there are a ton of great papers JAMS doesn't publish (due to severe page count constraints at the journal). Their reasoning is not "arbitrary"; it was spelled out quite clearly for the authors in the rejection notice they got. Many other papers in "trendy" subjects face the same fate.

Re: Formalising Mathematics: An Introduction

#65

Post by [deleted] »

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…

[deleted]

Re: Formalising Mathematics: An Introduction

#66

Post by dash2 »

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 what you tell them but can't typically "find their own way" to the proof of a theorem. Might these systems ever come down to my level?

Re: Formalising Mathematics: An Introduction

#67

Post by auggierose »

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…

Your argument is wrong in so many ways, but let me just show you one: A constructive proof guarantees that there is an algorithm, but it doesn't say anything about the runtime of that extracted algorithm. Now, what good is an algorithm that is much too slow to be practically useful?

In general, my hypothesis is that if you restrict yourself to constructive mathematics, you are limiting yourself. And that is true whether your chosen field is algorithms, or not.

Now, if you offer me for a given algorithm a constructive proof, that's great. But if you needed 10 years to give me that proof, and a non-constructive one can be had in 10 minutes, I might not be so enthusiastic if I had to pay your salary, or if I needed that result really urgently, or both. But on the other hand, IBM probably doesn't care.

Re: Formalising Mathematics: An Introduction

#68

Post by IngoBlechschmid »

zozbot234 wrote: post #16
adamnemecek wrote: post #3

I wish these attempts were using constructive mathematics but I understand that that would turn away a lot of mathematicians.

AIUI, the Lean system does support constructive mathematics. You can add axioms and reasoning principles that make the system non-constructive, but they're entirely optional.

Yes, you are quite right, but the community around Lean's standard library heavily focuses on classical mathematics.

Re: Formalising Mathematics: An Introduction

#69

Post by QuesnayJr »

spekcular wrote: post #64
QuesnayJr wrote: post #46

Earlier quoted context omitted.

There was a notorious case that a paper by Wehring solving the largest outstanding question in lattice theory was rejected by JAMS despite glowing referee reports (and being pretty short). So it's pretty much an example of editors arbitrarily killing a paper. (It appeared in Advances in Mathematics.) You can see a letter to the editor of the Bulletin about it. Look at the affiliations of the people protesting the dec…

I don't really see a problem with this decision, though I am sympathetic to Wehrung. As the editors note, there are a ton of great papers JAMS doesn't publish (due to severe page count constraints at the journal). Their reasoning is not "arbitrary"; it was spelled out quite clearly for the authors in the rejection notice they got. Many other papers in "trendy" subjects face the same fate.

What do you think they say? "You're not well-connected, so we're rejecting you"? How do you think political decisions get defended in academia? For insiders, you listen to the referees. For outsiders, you invoke some vague criterion of lack of fit or lack of interest. And people can come along and say "If this field is important, why doesn't it appear in JAMS"? It's a self-fulfilling prophecy.

Re: Formalising Mathematics: An Introduction

#70

Post by rssoconnor »

Abhinav2000 wrote: post #21
adamnemecek wrote: post #3

I wish these attempts were using constructive mathematics but I understand that that would turn away a lot of mathematicians.

What is constructive mathematics for the layman?

A lot of responses are going to say something like "it is mathematics without using the law of the excluded middle, or proof by contradiction" or something like that. They are not technically wrong, but I'd like to offer a different perspective.

The constructive logic used in constructive mathematics is classical logic with two new connectives added: the constructive existential, and the constructive disjunction (which could be defined in terms of the constructive existential).

The constructive disjunction and constructive existential connective has semantics given by the BKH interpretation[1]. A proof of the constructive disjunction A + B is either a proof of A or a proof of B. A proof of the constructive existential Σn:N. P(n) is a pair where n is a natural number and p is a proof of P(n).

So constructive mathematics isn't classical mathematics hindered, but constructive mathematics is mathematics enhanced with a more expressive language. Naturally constructive mathematics tends to focus on theorems written in this more expressive language that make use of these new constructive connectives, rather than focusing on the classical fragment which is already well studied.

For the non-layman: we can see that the above interpretation is correct because the fundamental logical rules for universal quantification, implication, conjunction, false and true are all identical between classical and constructive logic. And, according to classical mathematicians at least, this set of logical combinatorics is complete. Thus the law of excluded middle holds, even in constructive logic, so long as you use the classical disjunction, which is defined in terms of conjunction, implication, and false. Similarly you can prove that proof by contraction, i.e. double negation elimination ¬ ¬A -> A is a theorem of constructive logic whenever A is a formula that does not use the constructive disjunction or constructive existential (where negation is defined in terms of implication and false).

For the all of the above, I'm particularly focused on first-order number theory, however all of the above carries over to higher-order theories, and I think it even holds for set theory (or at least some large part of set theory such as Zermelo set theory; I forget what happens with the replacement axiom). Higher-order constructive mathematics does come with the caveat that the Axiom of Choice is not a theorem of constructive mathematics even when it is phrased only using the classical existential.

[1]https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...

Post reply on HN