Ring of integers in quadratic fields

Stream: maths

[Riccardo Brasca]

Now that we have docs#QuadraticAlgebra, the computation of the ring of integers in a quadratic field should be pretty doable. This has come up yesterday here and here.

In December there is ItaLean2025 and I would like to give this as project, so please let me know if someone is already working on it.

@Barinder S Banwait @Kevin Buzzard @Cameron Rampell

[Kevin Buzzard]

This is a great project. I'll bear it in mind that you've "claimed" it! There is plenty to do here -- for example IIRC there are exercises in Marcus to do the same sort of thing for $\mathbb{Q}(n^{1/3})$ (which we can do using $\Z[X]/(X^3-n)$ or other things when it's not this).

[Anne Baanen]

I'm excited to get this into Mathlib finally! We did do this computation in ancient Lean 3 times but it never got merged into Mathlib. See: Q(√4m + 1) and Q(√4m + {2, 3})

[Barinder S Banwait]

I too would welcome rings of integers of quadratic number fields in Mathlib! @Riccardo Brasca Vai pure!

[Barinder S Banwait]

Also that other thread on how to make meaningful contributions to Lean you linked to was super interesting. Reflecting on the supportive answers given to @Cameron Rampell , it prompts me to give more context for my question two days ago.

[Barinder S Banwait]

A few years ago, after having gone through Mathematics in Lean, I felt that I really needed a project to work on; as @Damiano Testa noted on the other thread, such projects are "one of the best ways to learn Lean".

[Barinder S Banwait]

I decided to give myself the goal of formalizing the proof of the Ramanujan--Nagell theorem. This is an exponential diophantine equation, fully accessible by an undergraduate student studying a first course in Algebraic number theory. You work in the ring of integers of $\mathbb{Q}(\sqrt{-7})$, factorise the equation, deduce each factor is a power of 2 (outside of some easily-dealt-with corner cases), eliminate $x$, and deduce congruence conditions on $n$ that via elementary methods yield the result. It was one of my favourite results from Stewart and Tall's book Algebraic number theory and Fermat's Last Theorem (whose proof I was trying to formalise). Probably because Pell equations (another class of diophantine equations dealt with via ANT) had recently been put into Lean (which @Michael Stoll worked on), I thought this would be a modest, toy project to cut my teeth on.

[Barinder S Banwait]

I started out, got to the point where I needed to factorise 2 (as in my question the other day), and got stuck. I got busy with other non-Lean math projects and didn't return to it until about two months ago when I met @María Inés de Frutos Fernández at Oberwolfach, who helped me bring it up to latest mathlib. FWIW here's the current state.

[Barinder S Banwait]

I'm now motivated to continue working on and finishing this project. @Yaël Dillies mentioned that "many people here (including myself) would be very happy to guide you through your first formalisation project so long as the topic bears some relevance to research mathematics". So if anyone else is interested in this project and able to help guide it, I'd very much appreciate that!

[Kevin Buzzard]

(two_pow_min_seven_odd is false BTW)

[Xinzzz Li]

Thanks @Kevin Buzzard ! After adding the condition n ≠ 0, two_pow_min_seven_odd can be verified. Just create a pull request. Very happy to discuss with Barinder :smiley: