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

71–80 of 125 posts

Re: Formalising Mathematics: An Introduction

#71

Post by asdftemp »

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.

that is a neat demo with a lot of useful links! In fact, it seems that the Lean developers/community are very interested in new methods of achieving readability, and providing users with tools to build interfaces that scale up to the complexity of real workflows.

For example, Lean in vscode supports interactive html "widgets": https://youtu.be/8NUBQEZYuis?t=453

(at that timestamp, there's a quick introduction to their typical use at the moment).

lean4 is committed to all sorts of extensibility; here's a demonstration of the new macros: https://twitter.com/derKha/status/1354082976456441861. There have also been several instances of users implementing old lean3 features (for example, the `calc` tactic mode, which has unique syntax for proving (in)equalities) by simply defining new type classes and short macros.

Re: Formalising Mathematics: An Introduction

#72

Post by spekcular »

QuesnayJr wrote: post #69
spekcular wrote: post #64

Earlier quoted context omitted.

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.

You seem determined to believe that the rejection was for "political" reasons despite having no evidence for this claim. The quoted reasoning was not "lack of fit" or "lack of interest," it was lack of "interaction with other areas of mathematics." Going back to my first comment, there's a general sense in the community that this sort of interaction among mathematical subfields (or with physics) is prized in research, and it's one of a few criteria that form the sociologically dominant view of what constitutes "good mathematics." You might disagree with these criteria, but it's not hard to see why that paper might lose out to other excellent papers when judged by them. This doesn't look like politics (favoring "insiders") to me; it looks like the consistent application of a value judgment about what good research is.

Again, whether you think the criteria should be the way they are is a separate conversation.

Re: Formalising Mathematics: An Introduction

#73

Post by vmilner »

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'…

I remember when encountering my first (or one of my first) proof by contradiction (irrationality of sqrt(2), say) feeling unsatisfied because I didn't know how one could know that it was _your_ assumption that was wrong and not one of the more fundamental ones of mathematics.

Re: Formalising Mathematics: An Introduction

#74

Post by Someone »

auggierose wrote: post #26
kevinbuzzard wrote: post #24

Earlier quoted context omitted.

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'…

> This actually happened Oh wow! Was it an interesting theorem that got proved this way? Did it get proved in another, less controversial manner as well? Could you provide a pointer to it?

https://en.wikipedia.org/wiki/Riemann_hypothesis#Excluded_mi... lists 3 such proofs.

Re: Formalising Mathematics: An Introduction

#75

Post by [deleted] »

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…

[deleted]

Re: Formalising Mathematics: An Introduction

#76

Post by abhinav22 »

sgeisenh wrote: post #36
Abhinav2000 wrote: post #21

Earlier quoted context omitted.

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 esp…

Many thanks

Re: Formalising Mathematics: An Introduction

#77

Post by abhinav22 »

rssoconnor wrote: post #70
Abhinav2000 wrote: post #21

Earlier quoted context omitted.

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 (wh…

Thanks!

Re: Formalising Mathematics: An Introduction

#78

Post by abhinav22 »

ithinkso wrote: post #35
Abhinav2000 wrote: post #21

Earlier quoted context omitted.

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 ther…

Thanks

Re: Formalising Mathematics: An Introduction

#79

Post by enricozb »

kmill wrote: post #58
zozbot234 wrote: post #38

Earlier quoted context omitted.

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.

I know we've discussed on HN before whether the elegance of the negative fragment extends to practice, but something about Lean is that it doesn't have LEM as an axiom. It's a theorem following from (a version of) the axiom of choice, the existence of quotient types, proof irrelevance (proofs of the same theorem are equal), and proposition extensionality (logically equivalent propositions are equal). Lean doesn't let…

In case anyone is curious, the proof of LEM from AC is: Diaconescu's Theorem [0]

[0]: https://en.wikipedia.org/wiki/Diaconescu%27s_theorem#:~:text....

Re: Formalising Mathematics: An Introduction

#80

Post by vcdimension »

auggierose wrote: post #67
vcdimension wrote: post #63

Earlier quoted context omitted.

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 whet…

Hey, there's no need to by so impolite. My argument is not wrong, it's just a different argument to yours (which I fully understand, and is not difficult to grasp). Your example doesn't discount mine in any way; a slow algorithm is still better than no algorithm at all. The point about proving the correctness of an existing algorithm is moot, I'm talking about mathematical proofs which in themselve lead to algorithms. I'm not claiming we should abandon non-constructive mathematics, just that formalizing mathematics constructively leads to more useful algorithms. Similar to the argument that some programmers make about constraining themselves to think purely functionally in order to produce less buggy code. Goodnight.
Post reply on HN