Undergraduate number theory student projects

Stream: maths

[Kevin Buzzard]

I'm good at onboarding maths undergraduates. But it's a changing terrain. In 2018 the question from the UGs was "do we have undergraduate thing X" and my answer was almost always "no, but we want that in mathlib so why don't you go away and make it" and the answer to "I'm looking for a project to help me learn Lean at a higher level" was "great, can you make bundled subsemirings, just copy submonoids" and people could be really helpful towards driving this community project forwards.

Lately, mathlib-helping projects suitable for first year undergraduates have become much harder for me to construct. One of the reasons for this is that in the lean code I'm writing as part of my research, the issues I'm running into involve technical things like normal closures or complex calculations in an abelian category, and it's all a bit much for first years.

On the other hand, looking at what people like @David Loeffler and @Michael Stoll and @Chris Birkbeck are doing -- you're all engaging with mathematics that I learnt in Cambridge Part III and my experience with working at this level is that projects suitable for first year undergraduates do show up sometimes

[Kevin Buzzard]

If there is anyone who feels they might have a good project suitable for a first or second year undergraduate then I can supervise it as part of my summer projects this year. I'll be working with over 20 maths undergraduates. Obviously I have a few ideas for projects myself, mostly completely unrelated to mathlib.

[Chris Birkbeck]

I have a few ideas of things that undergraduates might want to have a look at. For example, proving that cotangent identity that comes up when one looks at modular forms : image.png

Or things like, how many elements does $\mathrm{GL}_2(\mathbb{F}_p)$ have and a few others. Mathematically, these should be fine and I don't think we have them in mathlib yet. Hopefully they aren't too hard to turn into lean...

[Kevin Buzzard]

Ie this is not a plea for projects, it's advertisement of a free service of some kind. Projects are eight weeks long and run through July and August. We'll have students of all abilities.

[Jason KY.]

Do you only want number theory related project ideas or anything 1st/2nd year level ideas will work?

[Kevin Buzzard]

Oh yeah anything in pure suitable for undergrads is fine, it's just that if it's number theory I'll do a better job of supervising it

[Alex J. Best]

Ideally would the projects involve the students having to learn some new (interesting) maths, or get better with Lean by doing stuff they are more familiar with?

[Kevin Buzzard]

Anything. Usually I'm very light touch, I suggest things and people just organically make teams and collaborate

[Kevin Buzzard]

But now it's harder to contribute to mathlib and parts of number theory are moving quite quickly right now

[Kevin Buzzard]

@Amelia Livingston @Ashvni Narayanan @María Inés de Frutos Fernández you are all doing "Part III level number theory" -- do you see any projects which an undergraduate could help with?

[Kevin Buzzard]

@Jujian Zhang and @Andrew Yang are there projects in algebraic geometry which would be suitable for undergraduates?

[Kevin Buzzard]

Are there things about commutative rings or topological spaces or orders that you need for schemes?

[Wrenna Robson]

I can make some cryptography-related suggestions, though it's not quite my area.

[Wrenna Robson]

Specifically the thing that comes to mind is the mathematics in this: https://arxiv.org/pdf/1711.04062.pdf

[Wrenna Robson]

Simply because it's a lot of relatively abstract stuff and I don't know how much we have even in a less-concrete form.

[Wrenna Robson]

I could put you in touch with Luca (defeo.lu) too. Even the non-algorithmic side of things (much more mathlibbable) would be good to get in there. And I think it's the right level.

[Jujian Zhang]

I think value criterion for separateness is within reach.

[Antoine Labelle]

I believe that there are still some low-hanging fruits in linear algebra that could make a great contribution to mathlib for a first or second year undergraduate.
This winter I realized as I was doing representation theory that we had very few properties of the trace of a linear map, and that it was very annoying to prove any of them since the trace was defined in terms of the matrix trace, so we had to drop down to matrices everytime. Therefore, I proved that the current definition was equivalent to the basis-free definition of the trace in docs#trace_eq_contract and used this to prove a bunch of basic properties that I needed.
It could be a great first project for someone to do the same with the determinant, i.e. prove that the current matrix definition is equivalent to the basis-free definition in terms of exterior powers (which would probably involve first improving the docs#exterior_algebra API). With that definition one could then prove a bunch of properties like how the determinant behaves with respect to docs#tensor_product.map or docs#linear_map.prod_map, etc.

[Andrew Yang]

Do we already have the definition of separated morphisms?

[Wrenna Robson]

Antoine Labelle said:

I believe that there are still some low-hanging fruits in linear algebra that could make a great contribution to mathlib for a first or second year undergraduate.
This winter I realized as I was doing representation theory that we had very few properties of the trace of a linear map, and that it was very annoying to prove any of them since the trace was defined in terms of the matrix trace, so we had to drop down to matrices everytime. Therefore, I proved that the current definition was equivalent to the basis-free definition of the trace in docs#trace_eq_contract and used this to prove a bunch of basic properties that I needed.
It could be a great first project for someone to do the same with the determinant, i.e. prove that the current matrix definition is equivalent to the basis-free definition in terms of exterior powers (which would probably involve first improving the docs#exterior_algebra API). With that definition one could then prove a bunch of properties like how the determinant behaves with respect to docs#tensor_product.map or docs#linear_map.prod_map, etc.

It's more about matrices, but - https://leanprover-community.github.io/mathlib_docs/data/matrix/rank.html could use some love.

[Wrenna Robson]

Specifically we could do with defining the row-rank and the column-rank of a matrix, showing they are equal, stating rank-nullity in terms of it...

[Oliver Nash]

I believe we still lack the connection between linear independence and the wedge product. See e.g., https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/determinant.20via.20exterior.20algebra/near/260678544

[Riccardo Brasca]

You can do stuff about quadratic fields. The computation of the ring of integers or something like that.

[Alex J. Best]

Riccardo Brasca said:

You can do stuff about quadratic fields. The computation of the ring of integers or something like that.

If you do end up doing this the student could coordinate with @Anne Baanen, we needed some cases of this already and have some WIP code on this.

[Eric Wieser]

Oliver Nash said:

I believe we still lack the connection between linear independence and the wedge product. See e.g., https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/determinant.20via.20exterior.20algebra/near/260678544

This might become a bit easier once I make exterior_algebra R M = clifford_algebra 0 (blocked currently by #14303), since then we have the new recursor docs#clifford_algebra.left_induction

[Riccardo Brasca]

Also we can define the discriminant of an extension of number fields. Currently we have docs#algebra.discr, the discriminant given by any family of vectors of any ring extension, and we know how it changes under change of basis, so what is missing is that a number field admits a power basis given by integral elements (then one can use docs#algebra.discr_eq_discr_of_to_matrix_coeff_is_integral to prove that if the base field is ℚ then it is well defined as an integer).

[Patrick Stevens]

Mathlib seems quite light on numerical analysis at the moment, and there was a Part 1B short course on Numerical Analysis in my time - we've got Gram-Schmidt, but as far as I can see (and e.g. from https://github.com/leanprover-community/mathlib/blob/28f7172e9677fd412cdd500c914d18d423846715/docs/undergrad.yaml) we don't yet have any numerical integration. This could have the nice property that the output is procedures you can actually evaluate/get meaningful answers out of/visualise.

[Patrick Massot]

Yes, it would be very nice to have basic numerical analysis in mathlib. I don't think we can hope to have effective implementations in Lean 3, but we can definitely prove theoretical properties, say of basic numerical integration methods.

[Alex J. Best]

Oh that reminds me of another nice project, it should be possible to make a nice implementation of interval or ball arithmetic, defining operations on intervals of reals as the smallest interval containing the operation applied to. One could then show some algebraic properties of these things (some form of associativity / commutativity may hold), and teach norm_num to simplify some expressions involving these things with rational endpoints. Would be nice to then use it to give some nice estimates of constants.

[Yaël Dillies]

I've gathered thoughts on this specific point. Let me collect them in a PR.

[Adam Topaz]

Jujian Zhang said:

I think value criterion for separateness is within reach.

@Jack McKoen do you want to give this a shot? Here's the proof from the stacks project https://stacks.math.columbia.edu/tag/01L0

[Joseph Myers]

We already have issues #1038 and #14781 for real number computation by approximation (something that works fine if you're willing to work out all the intermediate numerical bounds outside of Lean and reduce things by hand to steps that norm_num can do together with existing lemmas).

We have various results on basic arithmetic operations between a single number and an interval, in data.set.intervals.image_preimage (proved more generally than just for the reals, of course), but I don't think we have anything like that for arithmetic operations on two intervals.

[Jack McKoen]

Adam Topaz said:

Jujian Zhang said:

I think value criterion for separateness is within reach.

Jack McKoen do you want to give this a shot? Here's the proof from the stacks project https://stacks.math.columbia.edu/tag/01L0

Absolutely, this seems like a good challenge

[Yaël Dillies]

#14807 for intervals.

[Yaël Dillies]

I can easily define addition and subtraction on interval. Multiplication looks a bit harder, and division probably requires multi-intervals to be useful.

[Andrew Yang]

IMO a well-defined separated-ness needs a well-defined notion of closed immersions, which in turn needs sheaf of ideals, or at least we should know that for a ring map f: A -> B, f*O_{Spec B} is the sheaf of modules of B as an A-module.
I’m not sure if we are there yet?

[Andrew Yang]

I think it would be great to see a formalized Matsumura.
In particular, Serre’s normality criterion, Cohen-Macaulay rings, module of derivations, stuff on flat modules should all be useful in the future.

[Kevin Buzzard]

Oh hmm. There's this problem that nobody will define sheaves of modules because it involves a design decision and each one comes with disadvantages. Maybe sheaves of ideals are easier though? ;-)

[Reid Barton]

We are still missing

8. The Impossibility of Trisecting the Angle and Doubling the Cube

[Reid Barton]

Not sure if this is the sort of thing you have in mind for your summer projects but one thing I would like to see is--we have all these great theorems in mathlib that cover large parts of the undergrad curriculum, but it's not clear to me how easy it is to apply these theorems to example and exercises. For instance, can we prove that $\mathbb{Q}(\sqrt[3]{2})$ is not a normal extension? Can we check that a cubic polynomial is irreducible over $\mathbb{Q}$ using the rational root test? Can we prove that an irreducible cubic polynomial has Galois group $S_3$ or $A_3$ depending on whether its discriminant is a square?

[Reid Barton]

I'm imagining student projects where the main theorem of the project itself does not necessarily have to get contributed to mathlib, but the project still contributes by filling API gaps or possibly new tactics.

[Reid Barton]

I think anyone can make up large numbers of these projects by picking up a textbook and trying to do the exercises.

[Reid Barton]

(... as long as it's a textbook where the theory itself is already in mathlib in a satisfactory state; that's why I took Galois theory for my examples, but surely there are other areas that would work too)

[Kevin Buzzard]

Yeah another one of the projects does involve formalising an appropriate undergraduate textbook