bachelor thesis subjects

Stream: Lean for teaching

[Johan Commelin]

Now and then I get asked if there is something to do in formalising maths for a bachelor thesis. Have we made a list somewhere of suitable topics?

[Kevin Buzzard]

I don't know of an explicit list, but let me make a remark: when I was actively supervising number theory PhD students (and I guess I've supervised about 15 of these, and still do), the times when it was easiest to come up with PhD problems were the times I was working hardest myself on research, because if you work hard on research then the PhD-suitable problems just appear. Last week Patrick got me back working hard on the perfectoid project again with this big with_zero refactoring, and I have already run into UG level holes which @Sian Carey and @Amelia Livingston have filled / are filling as part of their summer projects.

One difficult thing about this issue though is that you have to be careful about who you tell. Amelia is just finishing something up, but if I start going on about it publically there's a chance that someone like Kenny will just come along and binge on the problem for 5 hours and make everything, and then Amelia loses the chance to make a PR to mathlib (because for undergraduates PR's are currency, right? "I made the theory of semisubwithzerobotlattices in Lean and it's in the maths library" is something you can put on a CV / personal statement (at least in my opinion).

In other words, I have some ideas about this but it's not always a good idea to post them publically, especially because I have undergraduates this summer and it's my job to occupy them.

To be frank, I don't see why algebraic closures can't be an example, or (real-valued) valuations on finite extensions of the p-adic numbers (by the time I've refactored valuations this theory will just drop seamlessly into the perfectoid project). @Chris Hughes I need alg closures. How do you feel about handing it over to an undergraduate, so it at least gets done, and then you can fix it up later? My understanding from the VU meeting is that a student of Sander is doing the theory of factoring of ideals in Dedekind domains, which was a great thing to find out because I was going to get Amelia to look at it when she finishes structure theory of f.g. modules over a PID.

Galois theory needs doing. This is also something which was somehow happening (under my watch) and now seems to be not moving. @Kenny Lau @Chris Hughes can we state the fundamental theorem of Galois theory in Lean yet? I advise using bundled subgroups to state it; Sian has made them.

I think we should formalise an entire undergraduate representation theory course, with an arbitrary alg closed field of char 0 as coefficients. Here's a challenge. Can you prove the $p^aq^b$ theorem in Lean? A group whose order has at most 2 prime factors is solvable. Can you prove that the sums of the squares of the degrees of the irreducible representations of a finite group equals the order of the group? Not only is this accessible, it's really important.

As a general rule we might think about the lofty goal of having every standard definition from a pure maths undergraduate degree, and the proof of every theorem from such a degree, in mathlib. As far as I know no theorem prover has got an entire undergraduate degree's worth of maths in -- take a look at the myriad answers to https://mathoverflow.net/questions/336367/real-manifolds-in-a-theorem-prover to see what I mean. I think that if in a few years' time we can be going round to pure mathematicians who are also heads of maths departments saying thing like "look, Lean has basically all the pure maths you teach your undergraduates" will be interesting, and no other system has tried that before.

With calculus we just have to wait until we're out of this Bochner integral hole. Can someone give me an informed opinion here? When I started asking about results such as "R[X] is Noetherian if R is Noetherian" a long time ago, and asking if we had polynomials, Mario and Johannes were quick to point me to mv_polynomial (polynomials in arbitrarily many variables). I argued strongly that we needed a basic database of results about polynomials in one variable and a specialised interface for that system. @Chris Hughes agreed with me and ultimately supplied it, and Kenny, me and others all instantly started working hard with it and we learnt loads of things about type class inference and interfaces and bundling etc, there were all sorts of questions such as "should "n'th coefficient" even have a name because it' just evaluation of the function used in the implementation at n". Doing basic stuff teaches us things. How about a theory of differentiation of functions of one variable up to the statement that a power series in one complex variable is differentiable within its radius of convergence? How about a theory of basic ODEs? The proof that sine and cosine are a basis for the space of solutions to $F''+F=0$?

For algebra there we need group cohomology in all degrees. This is a really basic example of a cohomology theory. And we need singular cohomology of a top space with arbitrary abelian group coefficients, plus the long exact sequence. There are loads of problems here which the community know about -- cf Reid's CDGA thread.

We want the sheaf of Kaehler 1-forms on a scheme. I don't see why an undergraduate can't do that. The trick here is to find a good universal predicate (look at me Patrick not calling it Stricklandization) for one-forms.

We want the group law on an elliptic curve.

We want that the space of modular forms of a fixed weight and level is finite-dimensional. This might be a monster. Why not look at the proof, figure out what we need, and do that instead? Wait, this might rely on a good theory of compact Riemann surfaces so we have to wait for the analysts.

We want Ext and Tor for modules over a ring.

We want a formally verified database of all groups of order at most 6, containing each group up to isomorphism exactly once. Amelia's work will help with the abelian case. Sure it's dec_trivial but there are better proofs, and I don't think dec_trivial will make it to 6.

We want a general theory of projective and flat modules over a ring, including cohomological criteria.

We want Euler's formula V-E+F=2. This sounds like a real challenge. I'm not 100% sure we want it, actually.

I am desperate for Frobenius elements and conj classes in Galois groups. If L/K is a finite Galois extension of global fields with discriminant d (an ideal of K) and different D (an ideal of L) then for all primes upstairs coprime to D I want an element, and for all primes downstairs coprime to d a conjugacy class of elements, of the Galois group.

I want simplicial homology and a proof of the simplicial approximation theorem.

I want projective 1-space. Kenny was apparently having trouble with this. I think the issue was glueing schemes.

I want a proof that projective morphisms are proper.

Is that enough to be getting along with? Once we have all those, I would say that the Leanization of the algebra/number theory part of Imperial's BSc degree is well under way. I think this is the way to go at the minute -- for the analysis / differential geometry we just have to wait for the experts to do the basics in the way that they think is best.

[Johan Commelin]

@Kevin Buzzard Thanks a lot for this massive braindump! It will surely be helpful.
The problem with bachelor projects in Germany is that there is a very strict 3 month deadline. I'm still struggling to see if Lean can be integrated in such a project. Most professors don't want to cut in the mathematical content. Anyways, those are not your problems. But it makes Lean bachelor projects in Germany quite a challenge, I think.