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

51–60 of 125 posts

Re: Formalising Mathematics: An Introduction

#51

Post by creata »

auggierose wrote: post #42
vcdimension wrote: post #41

Earlier quoted context omitted.

You still need to construct the algorithm in the first place, which is what a constructive proof does.

Sure, but you would not need to prove it in a constructive way. See, that is one of the problems with constructive mathematics. It not only requires you to write down the algorithm, but also to prove it constructively, although a non-constructive proof would be perfectly fine. In other words: constructivism is often overkill.

But everything you'd typically see in an algorithm has decidable equality, so proofs by contradiction are constructively justified, no?

Re: Formalising Mathematics: An Introduction

#52

Post by kmill »

auggierose wrote: post #29
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'…

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 depend on the truth of some statement during their executions, and there's no general algorithm to decide whether undefined behavior is happening. They depend on undecided facts, so you can't put them together into a single program that decides the result. (Maybe a slogan is "truth can be contingent, but data cannot be.")

In Lean syntax, this is an example type signature of something that takes two programs (h and h') that respectively take in the truth/proof of a proposition or its negation, along with a proof that there is at most one element of α, and produces that element. I don't think there's a way to write this definition in Lean without marking the definition noncomputable:

  def extract {p : Prop} {α : Type*}
    (h : p → α) (h' : ¬p → α)
    (unique : ∀ (x y : α), x = y) : α := sorry
(the sorry indicates a missing definition).

Re: Formalising Mathematics: An Introduction

#53

Post by uyt »

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 you had to do every step of algebra manually with a line of code each. (and to be fair, in the beginning it was necessary because you're developing the usual rules of algebra as you go, but even in the later levels after they tell you about the ring tactic there's still a lot of manual algebra you need to do) The search space seems small enough that even I was just mindlessly spamming rewrite/intro/apply/induction. Why can't a computer automate this completely.

And going in the other direction, I was hoping this would be a good tool to aid in proofwriting. But most of the "proof" I wrote was complete gibberish not meant for human consumption. I think the problem is because the code relies heavily on mutating a context that you can't see without using the lean UI.

Anyway, maybe the number game is just not a good intro to the full capabilities of lean and I am missing the point.

Re: Formalising Mathematics: An Introduction

#54

Post by auggierose »

creata wrote: post #51
auggierose wrote: post #42

Earlier quoted context omitted.

Sure, but you would not need to prove it in a constructive way. See, that is one of the problems with constructive mathematics. It not only requires you to write down the algorithm, but also to prove it constructively, although a non-constructive proof would be perfectly fine. In other words: constructivism is often overkill.

But everything you'd typically see in an algorithm has decidable equality, so proofs by contradiction are constructively justified, no?

I don't know! But I don't think so. Also think about other properties of an algorithm, like runtime, etc. You could have a non-constructive proof for the upper bound on the runtime, but not a constructive one.

Re: Formalising Mathematics: An Introduction

#56

Post by nynox »

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).

Re: Formalising Mathematics: An Introduction

#57

Post by [deleted] »

auggierose wrote: post #54
creata wrote: post #51

Earlier quoted context omitted.

But everything you'd typically see in an algorithm has decidable equality, so proofs by contradiction are constructively justified, no?

I don't know! But I don't think so. Also think about other properties of an algorithm, like runtime, etc. You could have a non-constructive proof for the upper bound on the runtime, but not a constructive one.

[deleted]

Re: Formalising Mathematics: An Introduction

#58

Post by kmill »

zozbot234 wrote: post #38
cjfd wrote: post #28

Earlier quoted context omitted.

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.

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 you construct things that materially depend on LEM however -- you can only use it to prove that already constructed things have desired properties.

Re: Formalising Mathematics: An Introduction

#59

Post by auggierose »

auggierose wrote: post #54
creata wrote: post #51

Earlier quoted context omitted.

But everything you'd typically see in an algorithm has decidable equality, so proofs by contradiction are constructively justified, no?

I don't know! But I don't think so. Also think about other properties of an algorithm, like runtime, etc. You could have a non-constructive proof for the upper bound on the runtime, but not a constructive one.

Here is an example: after inputing positive integers a, b and c, output all natural numbers n for which a^n + b^n = c^n.

My algorithm: If a + b == c then output 1. If a^2 + b^2 == c^2 then output 2. Stop.

This algorithm is correct, because Fermat's last theorem holds. Now, try to come up with a simpler algorithm than that, and one that in addition has a constructive proof.

Re: Formalising Mathematics: An Introduction

#60

Post by breck »

drdeca wrote: post #50
breck wrote: post #44

I will pay $3.14 to the first person that formalizes mathematics using only https://treenotation.org/ .

This appears to just be saying “using python style indentation to represent trees”? I don’t understand the significance. Like, yeah, you can express whatever tree you want that way. Plenty of other ways to represent trees. It’s a nice enough default if you don’t know anything about the sort of thing the tree will contain. But there’s a reason that when writing conditionals, we don’t put each symbol in the expression…

> But there’s a reason that when writing conditionals, we don’t put one symbol in the expression on their own line

I won't disagree with you. However when you zoom out and crunch the numbers, you'll find that although there are infinite expressions to put in conditionals, in practice an absolutely minuscule amount of those patterns are actually used.

Context free grammars are not free.

Better ways are coming.

Post reply on HN