Paulson's "small formalisation challenges"

Stream: general

[Stuart Presnell]

@Lawrence Paulson has issued a few "small formalisation challenges":

• de Bruijn on Filling boxes with bricks
• de Bruijn on Defining reals without the use of rationals
• Niven's 1-page proof that π is irrational
• Littlewood on Dissection of hypercubes, which is on @Freek Wiedijk's 100 problems list and was formalised in Lean by @Floris van Doorn.

[Yaël Dillies]

The second item has already been done in Lean twice(!) using Eudoxus reals (but it's not in mathlib yet). What's new is that we can now plug that representation onto docs#conditionally_complete_linear_ordered_field and get the isomorphism with ℝ for free.

[Moritz Doll]

The proof that $\pi$ is irrational should be rather easy to do, we have everything needed for that.

[Yakov Pechersky]

Is the challenge to formalize de Brujin's papers as they are, or more "spirit of the law", have something that fits the concept, like what Yael mentioned?

[Stuart Presnell]

@Lawrence Paulson says at the top of the post "I list a few proofs that I would like to see formalised", which suggests that it's these specific proofs themselves rather than just the theorems.

[Yakov Pechersky]

I've been doing a little work on the side for constructed "decimal" expansions of p-adics. I can try to start on the more abstract "Defining reals through subtracted decimal sequences"

[Johan Commelin]

What is the benefit of doing these challenges in Lean?

[Arthur Paulino]

Johan Commelin said:

What is the benefit of doing these challenges in Lean?

Same spirit of coding (programming) challenges, I believe

[Filippo A. E. Nuccio]

Johan Commelin said:

What is the benefit of doing these challenges in Lean?

I had the same question...

[Eric Wieser]

Possibly for the purpose of assembling a mini rosetta stone comparing different provers writing the same proof?

[Yaël Dillies]

This is already happening in combinatorics, as @Mantas Baksys and myself are formalizing the same results in parallel, with Isabelle and Lean respectively.

[Bhavik Mehta]

I have a proof that pi is irrational using Cartwright's proof, and wikipedia describes how they are similar proofs: https://en.wikipedia.org/wiki/Proof_that_%CF%80_is_irrational#Niven's_proof

[Moritz Doll]

did you ever PR it? I did not find anything in mathlib about irrationality of $\pi$

[Andrew Yang]

By the way, how far is mathlib from the full Lindemann–Weierstrass? I see that the proof of e being transcendental is formalized in lean but not in mathib.

[Johan Commelin]

It is PR'd in #3884 but needs adoption.

[Ruben Van de Velde]

Johan Commelin said:

It is PR'd in #3884 but needs adoption.

I'm trying to see if I can make it build again, at least: https://github.com/leanprover-community/mathlib/compare/some_transcendental_things-2?expand=1

[FR]

Andrew Yang said:

By the way, how far is mathlib from the full Lindemann–Weierstrass? I see that the proof of e being transcendental is formalized in lean but not in mathib.

I'm working on it. But I'm afraid that there is still much work to do before we can put it into mathlib.

[Bhavik Mehta]

Moritz Doll said:

did you ever PR it? I did not find anything in mathlib about irrationality of $\pi$

If you're interested, it's here: https://github.com/leanprover-community/mathlib/blob/irrational-pi/src/analysis/special_functions/trigonometric/pi.lean (includes some unnecessary changes to other files too) One of the reasons I haven't PRd it is because it would be nice to have a proof of the stronger result that pi^2 is irrational, which isn't too much more difficult using similar proofs

[Ruben Van de Velde]

Bhavik Mehta said:

Moritz Doll said:

did you ever PR it? I did not find anything in mathlib about irrationality of $\pi$

If you're interested, it's here: https://github.com/leanprover-community/mathlib/blob/irrational-pi/src/analysis/special_functions/trigonometric/pi.lean (includes some unnecessary changes to other files too) One of the reasons I haven't PRd it is because it would be nice to have a proof of the stronger result that pi^2 is irrational, which isn't too much more difficult using similar proofs

If you proved pi is transcendental, you could use transcendental.pow :)

[Bhavik Mehta]

Ruben Van de Velde said:

Bhavik Mehta said:

Moritz Doll said:

did you ever PR it? I did not find anything in mathlib about irrationality of $\pi$

If you're interested, it's here: https://github.com/leanprover-community/mathlib/blob/irrational-pi/src/analysis/special_functions/trigonometric/pi.lean (includes some unnecessary changes to other files too) One of the reasons I haven't PRd it is because it would be nice to have a proof of the stronger result that pi^2 is irrational, which isn't too much more difficult using similar proofs

If you proved pi is transcendental, you could use transcendental.pow :)

True, but I think that might take me slightly longer than the existing proof :)

[Kevin Buzzard]

Bhavik Mehta said:

Moritz Doll said:

did you ever PR it? I did not find anything in mathlib about irrationality of $\pi$

If you're interested, it's here: https://github.com/leanprover-community/mathlib/blob/irrational-pi/src/analysis/special_functions/trigonometric/pi.lean (includes some unnecessary changes to other files too) One of the reasons I haven't PRd it is because it would be nice to have a proof of the stronger result that pi^2 is irrational, which isn't too much more difficult using similar proofs

Perfect is the enemy of good, as Scott would say!

[Johan Commelin]

I think it's a lot more interesting that π is irrational then that π ^ 2 is irrational. The proper upgrade from "π is irrational" would be to "π is transcendental" as pointed out above. In other words: just PR it :grinning: