The Mechanics of Proof (opens in new tab)

I would think you’d generally need to have something interesting in mind that you think might be true before bothering to prove it. Certainly you’ll need it to be interesting if you want anyone else to notice. It’s trivial to generate an endless tree of true statements by just tree searching with whatever valid operators your proof system has.

How do you know the statement is true if you have not proven it to be true?

Proof of true statements and discovery of new true statements go hand in hand. This is also because the proof tells you something about why the theorem is interesting. Generating multiple true statements given a set of assumptions is not very interesting per se.

But yes, something like, "in your situation, this is an interesting conjecture" would be nice in a proof assistant. Maybe AI will get us there.

Question is: Is something true or not? If you can prove it then you know it is true. If you cannot prove it all you know is you cannot prove it. It still could be true, or false. So the best you can do is to TRY to prove it, and/or try to prove its negation.

As pointed out by others generating random true statements is not very interesting because you can generate such trivially by appending && true as many times as you want to the statement.

So in general you always want to prove something, because only that can tell you something about what is true and what is not.

Yes, easily, but they are infinite and, unlike a given statement, mostly uninteresting.

It’s easy to generate true statements, but difficult to generate interesting true statements. It’s humans who intuit statements they think might be true, or are convinced must be true, and where we’d like to have a formal machine-checked proof. That latter use case is the primary one for theorem-provers like Lean.

Let's say you want to prove a compiler correct. How do you express that as a thing you want to prove mathematically? Here us a possible way to do it:

BehaviourMC(compile(src)) = BehaviourE(src)

You are basically saying that the machine code behaviour of the compiled source should be identical to emulating the source directly.

You then need to define what you mean mathematically by machine code etc. until the goal is fully specified.

And then you prove it correct.

You are referring to https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculatio...

That's hilarious. It's the brick joke, in math. https://plantsarethestrangestpeople.blogspot.com/2012/01/bri... It's a great example, made terrible (for teaching) because the punchline is never explained.

Your excerpt left out key information, which is the secondary hypothesis that am+bn=1

Hint: what are a and b? I won't wait for you to find values that satisfy the hypotheses.

It's the same flavor as: assume a=b+1, and b=a+1. Then a-b=b-a You can prove that p=>q, sometimes, even if p is false. (Especially if p is false!)

A later chapter provides the punchline.

https://hrmacbeth.github.io/math2001/07_Number_Theory.html#t...

The point is that in order to prove something by contradiction, you must assume something that turns out to be false and see what you can derive from that assumption (ideally a contradiction). The last link in the sibling comments does indeed contain proofs that the given premise is impossible. Think about how you know that the square root of 2 is irrational.

It is correct, true, and funny. Funny in the way that it creates a seeming contradiction and your brain feels good when it solves it.

Nothing special is going on there, but it may be distracting if the joke doesn't land.

For me, the best route is to start with Functional Programming in Lean [1]. Get familiar with dependent type theory and Lean's syntax. Then go back to Lean's source code [2].

Lean is self-hosted, so the language is written in Lean. And it's well documented. Starting from the Prelude [3], all the way up to the language server (yes, Lean ships a parser combinator library and a JSON library with the language).

One caveat is that the toolchain version of the repo is the repo itself, so you'd have to follow the development guide [4] to set it up.

Also, this is different from the standard library std4 [5], which is actually not shipped with the language, but just a normal package developed and used as the standard library.

[1]: https://leanprover.github.io/functional_programming_in_lean/

[2]: https://github.com/leanprover/lean4

[3]: https://github.com/leanprover/lean4/blob/master/src/Init/Pre...

[4]: https://github.com/leanprover/lean4/blob/master/doc/dev/inde...

[5]: https://github.com/leanprover/std4

Your best bet lies with the introductory Functional Programming in Lean: https://lean-lang.org/functional_programming_in_lean/

What by Dijkstra, specifically?

Deligne probably invoked the language of set theory without thinking that it restrained him too much. Mathematicians seem to be terrible philosophers.