Hensel's lemma in terms of derivative

Stream: Is there code for X?

[Jz Pan]

Seems that we only have Hense's lemma for Zp and for Henselian local rings in mathlib

[Jz Pan]

I found something interesting in an old note of commutative algebra, partially prepared by me

[Jz Pan]

(1) Lift-polynomial-factorization version of Hensel's lemma:

2025-06-30 013853.png

[Jz Pan]

I think we don't have this version in mathlib yet. But I doubt the usefulness of it. I remembered that it's used in ramification behavior of local fields?

[Jz Pan]

(2) Hensel's lemma in terms of derivative

2025-06-30 014123.png

[Jz Pan]

This is the version in mathlib for Henselian local ring. We also have a slight stronger version for Zp in mathlib, but it's proved only for Zp (yet).

[Jz Pan]

(3) A stronger version of Hensel's lemma in terms of derivative, also the inverse of formal power series with respect to composition

2025-06-30 014424.png

2025-06-30 014452.png

[Jz Pan]

I think this is the most close to the Zp version in mathlib. It turns out that it can be generalized to I-adic complete rings.

[Jz Pan]

It even have several variable versions:

2025-06-30 014752.png

Maybe this will be useful in several variable formal groups.

[Jz Pan]

I don't know if (1) holds for Henselian local rings (defined by using (2))

[Jz Pan]

If someone is interested I can provide proofs (two full pages...)

[Antoine Chambert-Loir]

I believe one should formalize the whole of Raynaud's book on local henselian rings.

[Ruben Van de Velde]

Any particular "one" who should do this? :)

[Jz Pan]

Antoine Chambert-Loir said:

I believe one should formalize the whole of Raynaud's book on local henselian rings.

Wow, that's a huge project.

[Jz Pan]

Ruben Van de Velde said:

Any particular "one" who should do this? :)

No one unless one needs to use it...

[Antoine Chambert-Loir]

That may look like a huge project, but until such fundamental books have been formalized, any stuff in algebraic geometry will inevitably bump into missing stuff all the time. (In it, you have a fairly general and usable theory of hensel rings, and its applications, eg to the Main theorem of Zariski.)

[Kevin Buzzard]

I wonder when AI will be massively helpful for jobs like this.

[Antoine Chambert-Loir]

Come on, Kevin, Stochastic algorithms don't reason and AI is only useful to a limited number of people who make jobs more profitable to them while worse for those who do them.

[Kevin Buzzard]

Basically you're saying "we should manually translate a pretty much self-contained book into lean" and other people are saying "yeah but which human will actually do this" and I'm saying "I think one day a machine might be able to do quite a good first draft"

[Kim Morrison]

Antoine Chambert-Loir said:

Come on, Kevin, Stochastic algorithms don't reason and AI is only useful to a limited number of people who make jobs more profitable to them while worse for those who do them.

I'm really curious, @Antoine Chambert-Loir, about your take on the trinity auto-formalization output. Have you read it?

[Antoine Chambert-Loir]

Probably not, and maybe I should. Which paper are you referring to?

[Alex Kontorovich]

https://www.morph.so/blog/trinity

[Antoine Chambert-Loir]

OMG…

[Jihoon Hyun]

Just curious, @Jz Pan are you working on factorizing polynomials?

[Jz Pan]

Jihoon Hyun said:

Just curious, Jz Pan are you working on factorizing polynomials?

No, currently I'm not working on any of these Hensel's lemmas. The Zp version in mathlib suffices to me. But of course this is not a long time solution.

[Kim Morrison]

@Antoine Chambert-Loir, more specifically, https://github.com/morph-labs/lean-abc-true-almost-always/blob/main/ABCTrueAlmostAlways/ABCTrueAlmostAlways.lean, which was formalized from https://arxiv.org/pdf/2505.13991

[Kim Morrison]

There is of course no paper. That is not the nature of these things. :-)

[Anatole Dedecker]

Kevin Buzzard said:

Basically you're saying "we should manually translate a pretty much self-contained book into lean" and other people are saying "yeah but which human will actually do this" and I'm saying "I think one day a machine might be able to do quite a good first draft"

My two cents: I think a lot of people would love to do a lot of formalization if they could get (academic and financial) credit for it, and imo it would be a much better use of our ressources. Besides, we all know that the optimal way to write a textbook is not the optimal way to write a Lean file, and I worry that starting with a statement-by-statement translation of any textbook will lead us to unusable results.

[Anatole Dedecker]

I mean, I thought we all agreed that formalizing existing mathematics is both fun and nontrivial, so I don't get why we're trying so hard to get machines to do this job.

[Yaël Dillies]

I personally see a lot of value in getting machines to do the boring part of the job, like reformatting, filling in basic API, etc...

[Anatole Dedecker]

I get this, but isn't this the kind of task where we should have reliable hand-crafted automation rather than high-powered LLMs? Keep in mind that reviewing is a major bottleneck for us, so I think that deterministic tooling has a clear advantage in terms of reviewing time.

[Yaël Dillies]

Sure, I'm easy :slight_smile:

[Anatole Dedecker]

Maybe I don't understand your message, but I'm definitely not suggesting that this is an easy task. The use of "high-powered" to refer to LLMs was meant in a rather litteral meaning (as in, LLMs are high-powered in terms of money, compute power, etc...), not as an opposition between "powerful tools for hard tasks" and "trivial tools for easy tasks".

[Anatole Dedecker]

Sorry if that read as "what you're doing is easy and should be easy to automate", I do not think this at all. Instead, I think that you deserve reliable and deterministic tools to help you (and everyone else) in these tasks so that you don't have to triple-check that the machine did everything as you expected.

[Yaël Dillies]

Ah sorry, that's a :flag_united_kingdom:-ism: I mean that I am a priori happy with any solution that improves my productivity when writing Lean code (modulo some environmental and privacy concerns)

[Antoine Chambert-Loir]

That's a big modulo, you'll apparently agree.

[suhr]

Running a LLM locally solves the privacy problem. It limits your choice to smaller models though, since you can't fit models like deepseek r1 into a single rtx 4090.

[Antoine Chambert-Loir]

I wrote a blog post organizing my thoughts about this experiment.
https://freedommathdance.blogspot.com/2025/07/autoformalization-of-mathematical.html

[Alex Kontorovich]

Thanks Antoine, very interesting! (My guess for the name "Trinity" is that it doesn't come from the Matrix, but rather the nuclear test, as in, a new world now exists... however overblown such claims may be...) I'm curious: nevermind the AI hype; did you end up feeling that there was some benefit to using such systems to speed up formalization work, of the kind we experienced at the Simons meeting? (I certainly feel such a speed-up. I believe Terry does as well...)

[Antoine Chambert-Loir]

No, i'm sorry, i didnt feel any benefit at all, and while — obviously — I can't dismiss your feelings, I turn my back to the idea that they have net benefit. (Speed-up does not interest me.)

[Martin Dvořák]

Antoine Chambert-Loir said:

I wrote a blog post organizing my thoughts about this experiment.
https://freedommathdance.blogspot.com/2025/07/autoformalization-of-mathematical.html

Thank you very much for such an insightful blog post!

[suhr]

In my experience, LLMs are somewhat useful for translating things from one language to another (that includes from a native language to a computer language) when such a translation does not require any actual understanding. But translating statements is a small and boring part of formalization.

For the hard and fun parts of formalization LLMs are neither useful nor desirable.

[suhr]

https://www.youtube.com/watch?v=cyyR7j2ChCI seems to be a good demonstration by the way: Terry uses statements generated by copilot, but immediately throws away AI generated proofs since these proofs are nonsense.

[metakuntyyy]

Anatole Dedecker said:

I mean, I thought we all agreed that formalizing existing mathematics is both fun and nontrivial, so I don't get why we're trying so hard to get machines to do this job.

Because, given the opportunity, players will optimize the fun out of the game.

[metakuntyyy]

Reminds me of my friend who had excel sheets just to play WOW, he even had to learn the quadratic formula as a mathematically inept person just so he could game.

[Kim Morrison]

I think it is going to be more fun when the boring parts get done without your attention. (Hence grind, and hence hoping that as LLMs are already taking the tedium out of writing python, they will take the tedium out of the uninteresting parts of proofs.)

[Anh Nguyễn]

When would Trinity become available for user

[Ruben Van de Velde]

Anatole Dedecker said:

I mean, I thought we all agreed that formalizing existing mathematics is both fun and nontrivial, so I don't get why we're trying so hard to get machines to do this job.

As a skeptic myself, I guess I can see some appeal if you want to work towards Big Theorem X but that depends on 5 relatively basic textbooks, and formalizing all those first seems daunting. But then I'm still not convinced the trade-off is worth it

[Martin Dvořák]

I pretty much agree both with the content and with the sentiment of Antoine Chambert-Loir's blog post.
Even tho Trinity sounds interesting, I am not excited about using it as a tool, or seeing it used by my colleagues.

I don't dream of a future where I write more-detailed informal proofs.
I dream of a future where I write less-detailed formal proofs!

[Filippo A. E. Nuccio]

Antoine Chambert-Loir said:

I wrote a blog post organizing my thoughts about this experiment.
https://freedommathdance.blogspot.com/2025/07/autoformalization-of-mathematical.html

Thanks @Antoine Chambert-Loir , nicely written and very interesting read!

[Wrenna Robson]

Antoine Chambert-Loir said:

I wrote a blog post organizing my thoughts about this experiment.
https://freedommathdance.blogspot.com/2025/07/autoformalization-of-mathematical.html

I was thinking many of these thoughts - and then you'd already written them! How kind :)

[Wrenna Robson]

I have spent a bit of time (it is a persistent theme in my thesis) thinking about the meaning of formalization work - which not to get too high-falutin' is basically what I mean by trying to pin down the "OK, but why" of a given formalization. I think intuitively I don't see much use in a proof of some particular lemma broken down into incomprehensible lemmas with little structure and zero good and useful naming. Like - who is it for? Who benefits? What can be built from it? If a proof typechecks, but nobody will use the result, and there is no concievable reason for the result, why should anyone care?

[Wrenna Robson]

I find AIs are quite good at producing text I don't want to read, and that indeed no human particularly cares to read, and I think they're quite good at producing code I don't want to read and definitely don't want to run either. Seems plausible the same is true of proofs.

[Wrenna Robson]

I'm sure many of us have had the experience of proving some result that feels absolutely key, but in practice we rarely actually use that theorem in that form, because it isn't the one that is actually useful for building stuff out of (often a sign that I've built something wrong).

[Wrenna Robson]

It feels to me like that on a macro scale.

[Bhavik Mehta]

While I haven't looked at all the comments in this thread, I will say that this particular lemma was part of the plan in the ABC-Exceptions project (https://github.com/b-mehta/abc-exceptions), and was a blueprint node there since well before any AI involvement (https://b-mehta.github.io/ABC-Exceptions/blueprint/sect0001.html#prop:ABCTrivialBound). This is one of the five nodes of that project where the blueprint proof is essentially "go read another paper".

[Filippo A. E. Nuccio]

Antoine Chambert-Loir said:

I wrote a blog post organizing my thoughts about this experiment.
https://freedommathdance.blogspot.com/2025/07/autoformalization-of-mathematical.html

An interesting conference, isn't it, @Antoine Chambert-Loir ?
https://agents4science.stanford.edu/index.html
:slight_smile:

[Sébastien Gouëzel]

That's a joke, right? I'm afraid not...

[Filippo A. E. Nuccio]

I don't think so... but in the FAQ page they say something interesting:

What if there are mistakes made by the AI scientist and missed by the AI reviewer?

We anticipate that errors will happen, and studying them will be instructive. All submissions and reviews will be publicly available on OpenReview. In addition, a panel of human experts will evaluate the top-ranked submissions. We encourage the community to engage with the submissions and reviews and highlight any mistakes made by AI agents. Understanding these failure modes is a key goal of the conference.

[Yuyang Zhao]

#28168 I proved a version of Hensel's lemma. However, I am not an expert in this field. I would like to know which intermediate results and corollaries are useful.