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

31–40 of 125 posts

Re: Formalising Mathematics: An Introduction

#31

Post by spekcular »

QuesnayJr wrote: post #20
kevinbuzzard wrote: post #15

Earlier quoted context omitted.

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…

Finite graph theory is completely mainstream mathematics. There's a kind of elite provicialism that you sometimes see, where only the mathematics that's done at Harvard or wins the big prizes counts, and this is a good example. There are probably more people employed in math departments working on finite graph theory than there are working on the Langlands Program. Robertson and Seymour were too old to be eligible, b…

Buzzard's post suggests to me that when he says "mainstream," he means what the community at large thinks of as important and field-defining (cf. the sentence with important in it). He is totally correct here; in this sense finite graph theory is not mainstream mathematics.

Further, I don't think it is "elite provincialism" to point out this readily verifiable fact. Besides looking at the big prizes, we can look at any of the top journals (Annals, IHES, Inventiones, Journal of the AMS, Acta, whatever). You're not going to find a lot of finite graph theory there.

Now, I think we should separate the question whether it is the case that he's right about what mathematicians value from the question of whether it ought to be the case that the world is this way. As I just said, the answer to the first question is yes. I'd argue that the answer to the second question is also yes, but that's a whole different discussion.

Re: Formalising Mathematics: An Introduction

#32

Post by Abhinav2000 »

kevinbuzzard wrote: post #24
Abhinav2000 wrote: post #21

Earlier quoted context omitted.

What is constructive mathematics for the layman?

It's mathematics where certain kinds of proof by contradiction are not allowed -- if you want to prove that something exists because you want to use it, then you have to make it, you can't just say "let's assume it didn't exist and go on from there to deduce that 0 = 1 which is definitely wrong, so our assumption is wrong, so it exists, so let's use it". Here is the reason why it's obvious for mathematicians. If you'…

Thanks Kevin. It seems like having both approaches is more flexible and thus more general (which can hopefully only be a good thing?). One could always replace a proof by contradiction later with a direct proof, but there's definitely value in using it in the meantime (at least in my uneducated view).

p.s. could you let me know your e-mail so I can keep for future reference, as I'm also working on a hobby project for automated theorem solving.

Re: Formalising Mathematics: An Introduction

#33

Post by Abhinav2000 »

a1369209993 wrote: post #23
Abhinav2000 wrote: post #21

Earlier quoted context omitted.

What is constructive mathematics for the layman?

Roughly, that proving a statement of the form "For all a,b,c,..., there exists x,y,z such that some statement involving a,b,c,...,x,y, and z is true." requires actually constructing suitable x,y, and z given suitable a,b,c, etc to derive them from.

Thanks

Re: Formalising Mathematics: An Introduction

#34

Post by auggierose »

vcdimension wrote: post #27
kevinbuzzard wrote: post #9

Earlier quoted context omitted.

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…

AFAIK the advantage of constructivism is algorithms. Coq allows you to extract lisp/ML/Haskell programs. Perhaps we will be seeing the next generation of fully homomorphic encryption programs, or topological data analysis programs, automatically generated by Coq.

So what about an algorithm you verified in a non-constructive way?

Re: Formalising Mathematics: An Introduction

#35

Post by ithinkso »

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?

Constructive mathematics rejects the law of excluded middle.

In a non-constructive mathematics it is true that 'either A or not A is true' and that allows you to prove existence of objects with certain properties by disproving their non-existence (if it cannot not-exist then it has to exist, by the law of excluded middle). Constructive mathematics, on the other hand, says that that's not enough and to prove that there exist objects with some properties you have to prove their existence.

Re: Formalising Mathematics: An Introduction

#36

Post by sgeisenh »

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?

https://en.wikipedia.org/wiki/Intuitionistic_logic

If you are familiar with "Classical" logic, constructive math omits the law of excluded middle (e.g. "A or not A" must be true). In ZFC, the axiom of choice is omitted.

This leads to proofs that are not only a verification of some idea but also gives you the mechanism to compute the evidence. This is often described as "the computational content of proofs" and is especially valuable in the context of the Curry-Howard isomorphism: for every proof, there is a corresponding program (and vice-versa). This is the basis for formal verification of constructive proofs. When creating a proof in Coq, you are actually writing the corresponding program. And you can even extract the program in another general purpose programming language (usually OCaml in the context of Coq, but Haskell is also supported).

Re: Formalising Mathematics: An Introduction

#37

Post by zozbot234 »

a1369209993 wrote: post #23
Abhinav2000 wrote: post #21

Earlier quoted context omitted.

What is constructive mathematics for the layman?

Roughly, that proving a statement of the form "For all a,b,c,..., there exists x,y,z such that some statement involving a,b,c,...,x,y, and z is true." requires actually constructing suitable x,y, and z given suitable a,b,c, etc to derive them from.

With the proviso that the non-constructive statement '∃ x such that P(x)' can also be understood constructively as '¬∀ x ¬P(x)' which does not require constructing a suitable x, so classical proofs can be modeled without adding any extra axioms to the logic. (Clearly the two statements are classically, though not constructively equivalent).

Similarly, all classical uses of LEM (A ∨ B) can be understood as constructive statements of the form ¬(¬A ∧ ¬B).

Re: Formalising Mathematics: An Introduction

#38

Post by zozbot234 »

cjfd wrote: post #28
adamnemecek wrote: post #3

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

There does not seem to be any reason for mathematicians to be turned about by these engines using constructive mathematics. One can use excluded middle as an axiom and do all the classical mathematics one likes. What becomes much easier if the engine is constructive is telling which theorems depend on excluded middle and which do not.

This is in fact how Lean works - the basic logic is constructive and excluded middle is an "extra" axiom. But even that is not as elegant as just writing non-constructive statements in the negative fragment of the logic, where (AIUI) one can already reason classically with no need for extra axioms.

Re: Formalising Mathematics: An Introduction

#39

Post by QuesnayJr »

spekcular wrote: post #31
QuesnayJr wrote: post #20

Earlier quoted context omitted.

Finite graph theory is completely mainstream mathematics. There's a kind of elite provicialism that you sometimes see, where only the mathematics that's done at Harvard or wins the big prizes counts, and this is a good example. There are probably more people employed in math departments working on finite graph theory than there are working on the Langlands Program. Robertson and Seymour were too old to be eligible, b…

Buzzard's post suggests to me that when he says "mainstream," he means what the community at large thinks of as important and field-defining (cf. the sentence with important in it). He is totally correct here; in this sense finite graph theory is not mainstream mathematics. Further, I don't think it is "elite provincialism" to point out this readily verifiable fact. Besides looking at the big prizes, we can look at a…

Pointing to the top journals is again a statement about who is well-connected, so if anything it is further proof of my claim of elite provincialism. Mathematics has politics, like any other field, and it's politics that determine that the proof of the Robertson-Seymour Theorem appeared in the "Journal of Combinatorial Theory" and not JAMS.

The irony is that I suspect every single mathematician, elite or not, knows what the four-color theorem is, far more than could tell you what chromatic homotopy is, or state anything about the Langlands program beyond "Uh, it's something about number theory? And groups? Maybe?"

Re: Formalising Mathematics: An Introduction

#40

Post by spekcular »

QuesnayJr wrote: post #39
spekcular wrote: post #31

Earlier quoted context omitted.

Buzzard's post suggests to me that when he says "mainstream," he means what the community at large thinks of as important and field-defining (cf. the sentence with important in it). He is totally correct here; in this sense finite graph theory is not mainstream mathematics. Further, I don't think it is "elite provincialism" to point out this readily verifiable fact. Besides looking at the big prizes, we can look at a…

Pointing to the top journals is again a statement about who is well-connected, so if anything it is further proof of my claim of elite provincialism. Mathematics has politics, like any other field, and it's politics that determine that the proof of the Robertson-Seymour Theorem appeared in the "Journal of Combinatorial Theory" and not JAMS. The irony is that I suspect every single mathematician, elite or not, knows w…

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 experts for "quick opinions." Only if these opinions are sufficiently positive is the paper sent for a full referee report (again by an expert), and in most (but not all) cases the referee's suggestion is followed. So the picture of editors just arbitrarily killing papers they don't like is not accurate.

Further, it's not like no finite combinatorics/graph theory gets published in these journals. Just not a lot, because it's not sufficiently interesting/valuable to the broader community. (Annals of Math almost published Hales's proof of the Kepler conjecture, after all; eventually a proof appeared in another top journal.)

Also, re: connections, you can easily check the author affiliations for papers in these journals. There are plenty of people from universities that are not so well known. It's hardly an "old boys club."

Post reply on HN