Mathlib bumps

Stream: FLT-regular

[Ruben Van de Velde]

I'm working on a bump

[Riccardo Brasca]

Thanks! The last two or so I did went smoothly, but I didn't check if there was something I could remove, so it is possible we have things that are already in mathlib.

[Ruben Van de Velde]

Pushed

[Kevin Buzzard]

FLT irregular will be opening in April and there will be a blue node called FLT_three but the criterion for making it green will be "it's in mathlib"

[Riccardo Brasca]

I think the best way of taking care of p=3 is to do both case 1 and 2 by hand. Case 1 should be really elementary, it is enough to reason mod 9

[Riccardo Brasca]

Does anyone want to start a new mathlib file with this proof?

[Chris Birkbeck]

Isn't this the proof that Ruben did?

[Ruben Van de Velde]

I don't think so, I did Euler's

[Ruben Van de Velde]

Do you have a reference for the proof you have in mind, Riccardo?

[Riccardo Brasca]

We have a full proof, written by Ruben.

[Riccardo Brasca]

The point is which proof we want in mathlib

[Riccardo Brasca]

In my opinion a good approach is to prove case 1 by hand, and to follow the general strategy for case 2

[Riccardo Brasca]

The point is that proving that Z[...] is a PID will soon be trivial (in mathlib), and then the full proof shouldn't be hard

[Riccardo Brasca]

This is the same as Ruben's proof, but written using eiseinstein integres

[Ruben Van de Velde]

Riccardo Brasca said:

The point is that proving that Z[...] is a PID will soon be trivial (in mathlib), and then the full proof shouldn't be hard

I guess I'll wait for that :)

[Ruben Van de Velde]

Started another bump at https://github.com/leanprover-community/flt-regular/compare/bump-2024-02-04 but got stuck on a proof in 92. I may take another look later, but also feel free to work on it (but please mention it here)

[Ruben Van de Velde]

Pushed

[Riccardo Brasca]

Ruben Van de Velde said:

Riccardo Brasca said:

The point is that proving that Z[...] is a PID will soon be trivial (in mathlib), and then the full proof shouldn't be hard

I guess I'll wait for that :)

I've juste delegated #9084 (with a couple of minor comments). One it lands, the fact that ℤ[ζ₃] and ℤ[ζ₅] are PID will only need some glue to connect the discriminant with the absolute discriminant, it is done here.

[Riccardo Brasca]

It's merged.

[Riccardo Brasca]

If someone want to PR the connection between discriminant and absolute discriminant please go ahead, I don't have time for it right now.

[Riccardo Brasca]

Another week, another bump

[Ruben Van de Velde]

I was planning to look at the connection, but only got as far as making the flt5 branch compile again at https://github.com/leanprover-community/flt-regular/pull/new/FLT5.1

[Riccardo Brasca]

I've added the file FLT5.lean to master.

[Riccardo Brasca]

I think we have a reasonable plan for FLT3:

• PR absdiscr_odd_prime various generalization to prime powers (maybe understanding why we need synthInstance.maxHeartbeats 80000. This should be relately quick.
• PR the fact that cyclotomic fields are totally complex
• Deduce that the rings of integers are PID if p = 3 or 5 (immediate)
• Prove case I by hand (reasoning modulo 9)

Now, proving FLT3 shouldn't be very hard, see for example here page 84

[Ruben Van de Velde]

[Meta.synthInstance] [3.679014s] ✅ MonoidHomClass (↥(𝓞 K) →+* K) (↥(𝓞 K)) K

Wasn't Anne's work supposed to fix that?

[Kevin Buzzard]

#mwe ?

[Ruben Van de Velde]

No time to come up with one right now, though it seems map_pow was the biggest offender

[Kevin Buzzard]

I only asked because I didn't even know how to get the mathcal O notation

[Ruben Van de Velde]

Oh, NumberField

[Ruben Van de Velde]

Maximal working example is https://github.com/leanprover-community/flt-regular/commit/b1552ac459920efef0c4aa4329c20282e022af51

[Riccardo Brasca]

I think we still have troubles with subtypes. The bump came with a few new set_option max... :(

[Riccardo Brasca]

I am PRing absdiscr_odd_prime

[Riccardo Brasca]

#10492

[Riccardo Brasca]

And #10502 for the fact that cyclotomic fields are totally complex.

[Riccardo Brasca]

Mmm, maybe we can prove that any number field with a primitive root of unity (for n bigger than 2) is totally complex. The proof is literally the same.

[Riccardo Brasca]

I've added in #10540 the fact that 𝓞 ℚ(ζ₃) and 𝓞 ℚ(ζ₅) are PID.

[Riccardo Brasca]

Doing p=7 would be a nice experiment to test the number field API.

[Chris Birkbeck]

Oh great!

[Riccardo Brasca]

Actually we can really try 7: the Minkowski bound is 4, so we only need to check ideals that contain 2 or 3 (this is in mathlib).

Note that we have Dedekind Kummer, so:

• over 2 everything is rather easy, we have $\Phi_7 = (x^3+x+1)(x^3+x^2+1)$. Moreover $2 = (\zeta_7^3 + \zeta_7 + 1)(2\zeta_7^4+\zeta_7 + 1)$ and $2 = (\zeta_7^3+\zeta_7^2+1)(2\zeta_7+\zeta_7^2+1)$ so there nothing else to do.
• over 3 things can be a little more annoying, we need to prove that $\Phi_7$ is irreducible (maybe it's time to factor cyclotomic polynomials over finite fields in general).

[Kevin Buzzard]

Ruben Van de Velde said:

[Meta.synthInstance] [3.679014s] ✅ MonoidHomClass (↥(𝓞 K) →+* K) (↥(𝓞 K)) K

Wasn't Anne's work supposed to fix that?

#10131 just landed -- does this help?

[Kevin Buzzard]

Doesn't appear to. What will help is Yury's suggestion to split off the OrderHom classes from the algebra heirarchy Hom classes. What's happening is that typeclass inference tries to figure out how it's going to find this MonoidHomClass, and so it has a look at what's available, and it finds this:

    [] new goal MonoidHomClass (↥(𝓞 K) →+* K) _tc.0 _tc.1 ▼
      [instances] #[@MulRingSeminormClass.toMonoidHomClass, MulEquivClass.instMonoidHomClass, @MonoidWithZeroHomClass.toMonoidHomClass, @RingHomClass.toMonoidHomClass, @MulSemiringActionHomClass.toMonoidHomClass, @OrderMonoidHomClass.toMonoidHomClass, @MulCharClass.toMonoidHomClass, @ContinuousMonoidHomClass.toMonoidHomClass]

And now, because the algorithm has the possibly dubious property that it tries the most recent instances first, it now spends a stupid amount of time trying and failing to find a topology or an order structure on O_K, despite the fact that no order or topology is mentioned anywhere in the question :-( This seems to basically be a fundamental difference between the way a human would go about solving this problem, and the way a computer attempts to do it.

What we want it to find is RingHomClass.toMonoidHomClass so you as a workaround while we're waiting for Yury's refactor, you can do

import Mathlib

variable (K : Type*) [Field K] [NumberField K]

open NumberField

attribute [instance 10000] RingHomClass.toMonoidHomClass -- go this way, typeclass inference system!

#synth MonoidHomClass (↥(𝓞 K) →+* K) (↥(𝓞 K)) K -- now fast

[Kevin Buzzard]

Oh I've just seen that #10544 is merged -- does this help? I'm not at lean right now.

[Ruben Van de Velde]

I can't easily compare apples to apples, but it seems like this is what it's now:

 [Meta.synthInstance] [0.340808s] ✅ MonoidHomClass (↥(𝓞 K) →+* K) (↥(𝓞 K)) K

so something must have helped

[Kevin Buzzard]

This is not fixed for me -- I suspect you're not importing mathlib (because nobody ever made a mwe). Here's mine:

import Mathlib

variable (K : Type*) [Field K] [NumberField K]

open NumberField

set_option synthInstance.maxHeartbeats 80000
set_option trace.profiler true
#synth MonoidHomClass (↥(𝓞 K) →+* K) (↥(𝓞 K)) K

This still needs a heartbeat bump on master. The trace is

[Elab.command] [2.109380s] #synth MonoidHomClass (↥(𝓞 K) →+* K) (↥(𝓞 K)) K ▼
  [step] [0.028240s] expected type: <not-available>, term
      MonoidHomClass (↥(𝓞 K) →+* K) (↥(𝓞 K)) K ▶
  [Meta.synthInstance] [2.074304s] ✅ MonoidHomClass (↥(𝓞 K) →+* K) (↥(𝓞 K)) K ▼
    [] [0.013681s] ✅ apply @Subalgebra.toRing to Ring ↥(𝓞 K)
    [] [0.012201s] ❌ apply @Subalgebra.normedCommRing to NormedCommRing ↥(𝓞 K) ▶
    [] [0.023935s] ❌ apply @IntermediateField.toField to Field ↥(𝓞 K) ▶
    [] [0.033890s] ✅ apply @IsDedekindDomain.toIsDomain to IsDomain ↥(𝓞 K) ▶
    [] [0.018440s] ✅ apply @Subalgebra.isDomain to IsDomain ↥(𝓞 K) ▶
    [] [0.108726s] ❌ apply @Field.isDomain to IsDomain ↥(𝓞 K) ▶
    [] [0.093777s] ❌ apply @DivisionRing.isDomain to IsDomain ↥(𝓞 K) ▶
    [] [0.050767s] ❌ apply @LinearOrderedRing.isDomain to IsDomain ↥(𝓞 K) ▶
    [] [0.251847s] ✅ apply @SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing to IsDomain ↥(𝓞 K) ▶
    [] [0.142327s] ❌ apply EuclideanDomain.instIsDomainToSemiringToCommSemiringToCommRing to IsDomain ↥(𝓞 K) ▶
    [] [0.020983s] ❌ apply Field.henselian to HenselianLocalRing ↥(𝓞 K) ▶
    [isDefEq] [0.010492s] ✅ ?m.11383 =?= Subalgebra.isDomain (𝓞 K) ▶
    [] [0.022462s] ❌ apply ValuationRing.of_field to ValuationRing ↥(𝓞 K) ▶
    [] [0.018256s] ❌ apply ValuationRing.of_field to ValuationRing ↥(𝓞 K) ▶
    [] [0.018425s] ❌ apply ValuationRing.of_field to ValuationRing ↥(𝓞 K) ▶
    [] [0.051782s] ❌ apply Field.instLocalRingToSemiringToDivisionSemiringToSemifield to LocalRing ↥(𝓞 K) ▶
    [] [0.032084s] ❌ apply @EuclideanDomain.to_principal_ideal_domain to IsPrincipalIdealRing ↥(𝓞 K) ▶
    [] [0.020320s] ❌ apply DivisionRing.isPrincipalIdealRing to IsPrincipalIdealRing ↥(𝓞 K) ▶
    [] [0.069415s] ✅ apply @SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing to IsDomain ↥(𝓞 K) ▶
    [] [0.012329s] ❌ apply EuclideanDomain.instIsDomainToSemiringToCommSemiringToCommRing to IsDomain ↥(𝓞 K) ▶
    [] [0.016732s] ✅ apply @IsDedekindDomain.toIsDomain to IsDomain ↥(𝓞 K) ▶
    [] [0.010505s] ❌ apply @DivisionRing.isDomain to IsDomain ↥(𝓞 K) ▶
    [] [0.069110s] ✅ apply @SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing to IsDomain ↥(𝓞 K) ▶
    [] [0.018049s] ❌ apply EuclideanDomain.instIsDomainToSemiringToCommSemiringToCommRing to IsDomain ↥(𝓞 K) ▶
    [] [0.016436s] ✅ apply @Subalgebra.isDomain to IsDomain ↥(𝓞 K) ▶
    [] [0.013637s] ✅ apply @IsDedekindDomain.toIsDomain to IsDomain ↥(𝓞 K) ▶
    [] [0.011247s] ❌ apply @Field.isDomain to IsDomain ↥(𝓞 K) ▶
    [] [0.010168s] ❌ apply EuclideanDomain.instIsDomainToSemiringToCommSemiringToCommRing to IsDomain ↥(𝓞 K) ▶
    [] [0.027972s] ✅ apply @IsDedekindDomain.toIsDomain to IsDomain ↥(𝓞 K) ▶
    [] [0.011063s] ❌ apply @LinearOrderedRing.isDomain to IsDomain ↥(𝓞 K) ▶
    [] [0.059016s] ✅ apply @SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing to IsDomain ↥(𝓞 K) ▶
    [] [0.018312s] ✅ apply @IsDedekindDomain.toIsDomain to IsDomain ↥(𝓞 K) ▶
    [] [0.061880s] ✅ apply @SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing to IsDomain ↥(𝓞 K) ▶

so it's just a shedload of things taking 0.05 seconds and it all adds up. When you dig further in, the trace is just full of things like

[] [0.122424s] ✅ CommRing.toRing =?= Function.Injective.ring Subtype.val _ _ _ _ _ _ _ _ _ _ _ _

:-( I'll start a new thread in #mathlib4

[Ruben Van de Velde]

Oh yeah, the bad case was importing Mathlib. Sorry for the lazy test

[Riccardo Brasca]

Riccardo Brasca said:

I think we have a reasonable plan for FLT3:

• PR absdiscr_odd_prime various generalization to prime powers (maybe understanding why we need synthInstance.maxHeartbeats 80000. This should be relately quick. Now in mathlib.
• PR the fact that cyclotomic fields are totally complex #10502
• Deduce that the rings of integers are PID if p = 3 or 5 (immediate) #10683
• Prove case I by hand (reasoning modulo 9) #10698

Now, proving FLT3 shouldn't be very hard, see for example here page 84

I've proved case 1 in #10698. Now all the prerequisites are PRed, we can think about a serious plan to done FLT3 once and for all.

[Riccardo Brasca]

I guess the next nontrivial step is to find the 6 units of $\mathbb{Z}[\zeta_3]$.

[Chris Birkbeck]

At some point we used something like this right? I remember we had an argument that used the totient function

[Riccardo Brasca]

To compute the units? I have no idea

[Chris Birkbeck]

We had a result that says the only units in these cyclotomic fields was +- the zeta_3

[Riccardo Brasca]

Ah, nice!

[Riccardo Brasca]

Anyway using docs#NumberField.isUnit_iff_norm it shouldn't be too hard.

[Chris Birkbeck]

This is what I had in mind : https://cbirkbeck.github.io/FltRegulartest/doc//FltRegular/NumberTheory/Cyclotomic/UnitLemmas.html#roots_of_unity_in_cyclo

[Riccardo Brasca]

OK, good. This seems something we can put in mathlib in full generality.

[Riccardo Brasca]

#10710 is a polished version of what we have in the project. We will need some glue to connect this with units, but it should be straightforward.

[Riccardo Brasca]

I am bumping mathlib, and because of #10640 there a couple of changes. Nothing serious, but does anyone have a clear and definite answer about the recommended style for suffices? Is the following

example (h : 2 = 3) : 1 + 2 = 1 + 3:= by
  suffices 2 = 3 by
    rw [this]
  exact h

what we are supposed to write?

[Damiano Testa]

I think that it is

  suffices this : 2 = 3 by
    rw [this]

At least, I see syntax like this in #10640.

[Riccardo Brasca]

Yes, you syntax also works. But I have another question: writing a proof like this, I don't know how to make this visible in the infoview (when I am proving that it is enough to prove the main goal assuming this). Note that if you already have the full proof this seems ok (the infoview is working), but not when you are writing it. I mean that

example (h : 2 = 3) : 1 + 2 = 1 + 3:= by
  suffices this : 2 = 3 by
    --the cursor is here, and there is no `this` in the infoview

[Riccardo Brasca]

example (h : 2 = 3) : 1 + 2 = 1 + 3:= by
  suffices this : 2 = 3 by
    ·  --putting the cursor here makes the infoview working

[Damiano Testa]

That is annoying. I wonder whether there is a missing focus missing in the syntax somewhere...

[Damiano Testa]

If you add

macro "suffices " d:sufficesDecl : tactic =>
  `(tactic| refine_lift suffices $d; focus ?_)

before your example, you get the behaviour that you expect, right?

[Riccardo Brasca]

I get an error about focus.

[Riccardo Brasca]

Anyway if someone else confirms that I am not doing something completely stupid I can just ask in general

[Damiano Testa]

Is it because you have no imports?

[Riccardo Brasca]

I have imported a pretty deep file in mathlib just to be in a real life scenario, but no import Mathlib (that in practice ignores #10640)

[Damiano Testa]

Ok, I think that I was seeing different things, since I have the habit of placing an underscore to get better messages:

import Mathlib.Tactic

example (h : 2 = 3) : 1 + 2 = 1 + 3:= by
  suffices this : 2 = 3 by
    _

if you position your cursor before the _ you should see this, right?

[Riccardo Brasca]

Yes, with the _ it works

[Damiano Testa]

Ok, in any case, I agree that it is annoying behaviour!

[Damiano Testa]

Btw, it seems to work from the second line of the proof:

example (h : 2 = 3) : 1 + 2 = 1 + 3:= by
  suffices this : 2 = 3 by
    have := this

[Damiano Testa]

Riccardo Brasca said:

Note that if you already have the full proof this seems ok (the infoview is working), but not when you are writing it.

I guess that my last comment was implied by ^ comment of yours.

[Ruben Van de Velde]

I tend to write done there

[Damiano Testa]

I fear that this is another instance of "Lean cannot give good error messages, since its syntax is too extensible".

[Riccardo Brasca]

To be honest I don't care that much about good error messages, but what is a convenient workflow to write a proof using suffices?

[Riccardo Brasca]

I mean, I would like to see this in the infoview when writing the proof.

[Riccardo Brasca]

Ruben Van de Velde said:

I tend to write done there

Do you mean instead of the _?

[Ruben Van de Velde]

Riccardo Brasca said:

Ruben Van de Velde said:

I tend to write done there

Do you mean instead of the _?

Yeah

[Yaël Dillies]

Should we should restore the old suffices syntax?

[Riccardo Brasca]

Please don't bump mathlib in the next 10 days. It is at the same version of the lftcm2024 repository and I would like to keep it like that during the conference.

[Chris Birkbeck]

The blueprint is broken at the moment, but I have a fix coming.

[Riccardo Brasca]

Thanks!

[Chris Birkbeck]

Alright it's working again :)

[Riccardo Brasca]

I wanted to bump mathlib to the new Lean version but I get

lake update

mathlib: updating repository './.lake/packages/mathlib' to revision '4e159e0ef38e6e7894342429440ec9b4f5011bfd'
std: updating repository './.lake/packages/std' to revision '3025cb124492b423070f20cf0a70636f757d117f'
aesop: updating repository './.lake/packages/aesop' to revision '0a21a48c286c4a4703c0be6ad2045f601f31b1d0'
proofwidgets: updating repository './.lake/packages/proofwidgets' to revision 'fe1eff53bd0838c657aa6126fe4dd75ad9939d9a'
Cli: updating repository './.lake/packages/Cli' to revision 'a11566029bd9ec4f68a65394e8c3ff1af74c1a29'
importGraph: updating repository './.lake/packages/importGraph' to revision '188eb34fcf1125e89d651ad462d02598219718ca'
warning: Qq: ignoring missing dependency manifest './.lake/packages/Qq/lake-manifest.json'
error: ./.lake/packages/proofwidgets/lakefile.lean:35:4: error: function expected at
  FetchM
term has type
  ?m.2162
error: ./.lake/packages/proofwidgets/lakefile.lean:70:4: error: function expected at
  FetchM
term has type
  ?m.2226
warning: ./.lake/packages/proofwidgets/lakefile.lean:82:7: warning: declaration uses 'sorry'
warning: ./.lake/packages/proofwidgets/lakefile.lean:85:7: warning: declaration uses 'sorry'
error: ./.lake/packages/proofwidgets/lakefile.lean: package configuration has errors

[Riccardo Brasca]

Can someone try to do the same to check if the fault of my installation?

[Ruben Van de Velde]

:eyes:

[Chris Birkbeck]

I got the same error

[Riccardo Brasca]

OK, posting in #general

[Patrick Massot]

Are you sure you have the same toolchain in your project and in mathlib?

[Ruben Van de Velde]

I got past this, but it doesn't seem like doc-gen is on 4.8 yet

[Riccardo Brasca]

The project is currently on leanprover/lean4:v4.7.0 with a working mathlib (commit e9bc16347b34a91a7498edb615179b5788bf1ed4). I just wanted to bump mathlib, via lake update, and I got that error.

[Ruben Van de Velde]

Yeah, but mathlib moved to 4.8. I'll push initial fixes in a bit

[Riccardo Brasca]

Yes, that was my point, to update it. I've always used lake update IIRC

[Chris Birkbeck]

I had to manually change it to 4.8.0-rc1 but still not working :(

[Ruben Van de Velde]

https://github.com/leanprover-community/flt-regular/pull/new/v4.8.0

[Ruben Van de Velde]

Not finished yet, but I need to step out for a few hours, so feel free to continue

[Riccardo Brasca]

I will not have time to work on this until tomorrow, but I can do it. Especially if the weird problem with lake update is solved.

[Ruben Van de Velde]

I manually updated the manifest, so the update issue no longer gets in the way

[Ruben Van de Velde]

https://github.com/leanprover-community/flt-regular/pull/103 should build now, but I don't have enough battery to to another full build, so it would be nice if someone could verify

[Riccardo Brasca]

There is now an error building documentation, I guess something it's not updated to 4.8

[Ruben Van de Velde]

Oh yeah, I threw out the doc-gen dependency because I didn't find a compatible version.

... I wonder if the mathlib docs are working

[Ruben Van de Velde]

RingOfIntegers landed, so I guess we need another bump

[Riccardo Brasca]

I just started working on it, but I am not able to download mathlib cache

[Riccardo Brasca]

I only get half of it

[Riccardo Brasca]

Fixed

[Riccardo Brasca]

I've started the bump in the branch bumpRingOfInt. It's a bit annoying but nothing really problematic (there is probably a norm_cast attribute missing).

[Riccardo Brasca]

I have to stop now, and I will not have time tomorrow. If someone wants to work on this, the next file is FltRegular/NumberTheory/KummersLemma/Field.lean that has quite a lot of errors.

[Riccardo Brasca]

Note that I have removed

instance : CharZero (𝓞 K) := SubsemiringClass.instCharZero (𝓞 K)

but now inferInstance works.

[Ruben Van de Velde]

Same here, I just pushed a note where KummersLemma.Field starts to go wrong

[Riccardo Brasca]

I've made some progress, the next file is Hilbert92.lean: I've started working on it but I have to stop.

[Riccardo Brasca]

The bump is done.

[Chris Birkbeck]

Ah thanks for sorting this!