Frobenius endomorphism

[tirix]

Simple theorem about the Frobenius endomorphism.

[metakunt]

Nice @tirix that is excellent. I am sorry I was busy working during the weekend so I didn't have much time.

What I did is some research based on your blueprints. I have found that lean4 uses blueprints and uses the library mathlib4. I am trying to understand tactics and learn how to write theorems in lean. Maybe we can study which theorems are in mathlib4 so that we have a grasp of what is needed for the formalization.

I thought about trying to formalize AKS in lean, see what theorems we actually need and port them over.

https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/Galois.html#IsAlgClosure.isGalois

It appears to have results, but I am not yet well versed in how to understand them. But this theory appears to be formalized in mathlib, maybe we can take a similar approach to metamath.

What do you think?

[tirix]

What do you think?

Yes, checking how Galois Theory has been formalized in Lean might be a good idea. I have not checked that.

A textbook reference we've been using for algebra is [Lang]. It also develops the theory of Galois Theory, and algebraic closure. See chapter V.2, p. 229 for the algebraic closures, and chapter V.5. p. 244 for finite fields.

Actually I most of the ground work has already been formalized (we have groups, rings, modules, polynomials), so this is really the next chapter of the book to be formalized.

[tirix]

PS. the Frobenius endomorphism is used in AKS, in the proof of Claim 1.i. of theorem 6.1, so this can be useful in the future.

[icecream17]

That website is an amazing reference. Good find. The syntax looks similar to Agda so I can kinda understand it.

It doesn't provide the implementation definitions and proofs directly, but rather the types and explanations of what each thing is, and gives a link to the source for further detailing.

[metakunt]

Yeah I don't yet understand it fully, but I am learning it so that I can try to reprove the statements I did in metamath and port it over to lean4. I want to see how much more easy/difficult it is.

Currently lean4 has some pluses that metamath doesn't have, like modularity, tooling, bigger library and way more speed once you learn it.

Metamath however has way more understandability, since every step is clear in the open. It is much more detailed and once you understand it you just need to find the fitting theorems. It works as the types are what they are and they are not in a way dynamic typed. For example in metamath + is for complex numbers only whereas in lean + is overloaded for a variety of operations. This has both its pros and cons. I think the lean tooling is excellent and from what I've seen the automatism of tactics closes many goals that would in metamath be few minutes in one tactic.

One example is the tauto tactic. Assume you have 2 propositional statements that you want to show are equal in a sense that they produce the same truth table. In lean it is just this one tactic and the goal is closed, whereas in metamath you would need a few steps and you would need to put some thought into it.

But it also sadly has one glaring downside is that it is so much harder to learn. The cliff I have to jump over lean is so much higher than the cliff I had to jump when I started learning metamath. In metamath I could basically start with some advice from @tirix and some questions and I was good to go. In lean I have atleast 40 questions/things I want to ask/do and I haven't even written down any.

Also another downside is that much of the documentation is still for lean3, however lean3 is deprecated and you should only use lean4. That has its annoyances as a newcomer that you don't know that you are copying lean3 code and wondering why it doesn't work.

[digama0]

On Sun, Jun 2, 2024 at 1:43 PM metakunt @.***> wrote:

But it also sadly has one glaring downside is that it is so much harder to learn. The cliff I have to jump over lean is so much higher than the cliff I had to jump when I started learning metamath. In metamath I could basically start with some advice from @tirix https://github.com/tirix and some questions and I was good to go. In lean I have atleast 40 questions/things I want to ask/do and I haven't even written down any.

Also another downside is that much of the documentation is still for lean3, however lean3 is deprecated and you should only use lean4. That has its annoyances as a newcomer that you don't know that you are copying lean3 code and wondering why it doesn't work.

On this point in particular I highly recommend taking advantage of https://leanprover.zulipchat.com/ where there are lots of people (including me) willing to help out with questions of all kinds. But yes, it's definitely true that there is a lot more to learn to get good at using lean compared to metamath.

Message ID: @.***>

[tirix]

The metamath community is way smaller than the Lean community, and so we are also much slower to get better tools. Anyway I've created a Zulip organization at https://metamath.zulipchat.com/, maybe this can also help communication.

Lots of discussion unrelated to the actual PR! :) Can I merge?

[icecream17]

The metamath community is way smaller than the Lean community, and so we are also much slower to get better tools. Anyway I've created a Zulip organization at https://metamath.zulipchat.com/, maybe this can also help communication.

Lots of discussion unrelated to the actual PR! :) Can I merge?

The chat needs an invitation, apparently

[icecream17]

the conflict is actually in my mathbox because of the ring structure deductions I added in #4029 (specifically this commit: https://github.com/metamath/set.mm/pull/4029/commits/18e51d7ed6526e894a0f67a21b0dfde034ff9b84) I don't have write access to resolve the conflict though.

The editorial is not needed anymore now that ringgrpd is moved, so:

  ${
    ringabld.1 $e |- ( ph -> R e. Ring ) $.
    $( A ring is an Abelian group.  (Contributed by SN, 1-Jun-2024.) $)
    ringabld $p |- ( ph -> R e. Abel ) $=
      ( crg wcel cabl ringabl syl ) ABDEBFECBGH $.

    $( A ring is a commutative monoid.  (Contributed by SN, 1-Jun-2024.) $)
    ringcmnd $p |- ( ph -> R e. CMnd ) $=
      ( ringabld ablcmnd ) ABABCDE $.
  $}

[tirix]

The chat needs an invitation, apparently

I've changed the settings, you should be able to join.

[tirix]

the conflict is actually in my mathbox

Thanks, I'll do the merge.