## Stream: maths

### Topic: Suggestions for maths/computing projects

#### Kevin Buzzard (Sep 29 2018 at 11:58):

In the UK the system is that the undergraduates come into university having chosen their major and can only do classes offered by the corresponding department(s). The third year undergraduates doing a joint maths/computing degree hence know quite a bit of maths and CS. I have been asked to suggest possible projects for these students. No other pure mathematicians ever get involved. If anyone has any suggestions for projects they they think might be appropriate then I would be very interested to hear them.

#### Kevin Buzzard (Sep 29 2018 at 11:59):

I think 4th years can also take them so MSc level is ok

#### Kevin Buzzard (Sep 29 2018 at 12:01):

I will suggest a homological algebra project and a project to make math.rat, a class for rational numbers which behaves like a number theorist thinks -- eg you can talk about a math.rat being prime or induct on it if it's known to be a nat etc

#### Kevin Buzzard (Sep 29 2018 at 12:02):

I'll suggest a number field / Galois theory project maybe

#### Mario Carneiro (Sep 29 2018 at 12:02):

I'm not sure why you need another type, like I mentioned before

#### Kevin Buzzard (Sep 29 2018 at 12:03):

But if there's anything mathsy that anyone wants done then let me know quick

#### Mario Carneiro (Sep 29 2018 at 12:03):

just define the typeclasses is_nat_prime, is_nat, is_rat on any nice type

#### Kevin Buzzard (Sep 29 2018 at 12:04):

Mario are you ok with a typeclass is_nat q on rat in mathlib?

#### Mario Carneiro (Sep 29 2018 at 12:04):

I think it should be generic in the type

#### Kevin Buzzard (Sep 29 2018 at 12:04):

I thought you had reservations about the Prime typeclass

On nat

#### Mario Carneiro (Sep 29 2018 at 12:05):

it says \ex n, nat.cast n = x, in whatever generality that statement makes sense

#### Kevin Buzzard (Sep 29 2018 at 12:05):

Is it ok if it's data?

sure

#### Mario Carneiro (Sep 29 2018 at 12:06):

the name is_nat is a bit misleading in that case, but I don't have a better suggestion

#### Mario Carneiro (Sep 29 2018 at 12:06):

at least it's a subsingleton (in char 0)

is_of_nat?

math.nat?

#### Mario Carneiro (Sep 29 2018 at 12:08):

I don't think I want to ever use math as a namespace

#### Mario Carneiro (Sep 29 2018 at 12:08):

if you do that it's like "wait, what were we doing before?"

#### Mario Carneiro (Sep 29 2018 at 12:09):

the_real_nat

#### Mario Carneiro (Sep 29 2018 at 12:09):

what about natural, integral etc?

#### Mario Carneiro (Sep 29 2018 at 12:10):

like "x is a natural element of A"

#### Reid Barton (Sep 29 2018 at 13:01):

How big a project are we talking about? Have you checked https://github.com/leanprover-community/mathlib/wiki/Potential-projects for ideas?

#### Reid Barton (Sep 29 2018 at 13:02):

One item I'd like to see that hasn't made it onto that list is covering space theory

#### Mario Carneiro (Sep 29 2018 at 13:04):

I actually went to some effort to do covering space theory in metamath a while back. The big theorem was existence and uniqueness of lifts; it was hard to find an appropriately general statement so it might be of use

#### Mario Carneiro (Sep 29 2018 at 13:06):

But we need simply connected and path connected spaces first

#### Mario Carneiro (Sep 29 2018 at 13:06):

also connectedness

#### Reid Barton (Sep 29 2018 at 13:15):

On an unrelated note,

just define the typeclasses is_nat_prime, is_nat, is_rat on any nice type

some lemmas like @[simp] lemma pos_of_is_nat_prime (p : rat) [is_nat_prime p] : p > 0 would make this padic norm stuff go a lot more smoothly

#### Reid Barton (Sep 29 2018 at 13:29):

though maybe this doesn't really require the class--I'm still unclear on how exactly simp tries to satisfy side conditions

#### Rob Lewis (Sep 29 2018 at 13:29):

Even just an is_prime class on nat would clean up the padic file a lot. Mario and I discussed this briefly in the first padics PR. I was planning to experiment with it soon.

#### Mario Carneiro (Sep 29 2018 at 13:30):

I am considering just marking prime itself as a class, without changing the theorems

#### Kevin Buzzard (Sep 29 2018 at 13:32):

One of my students wrote 1000 lines of Lean code on connectedness

#### Kevin Buzzard (Sep 29 2018 at 13:32):

and never really bothered to mention this to anyone

#### Kevin Buzzard (Sep 29 2018 at 13:32):

https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/Topology/Material/connected_spaces.lean

#### Rob Lewis (Sep 29 2018 at 13:34):

@Mario Carneiro That would certainly work. I wonder if we'd eventually end up duplicating the statements of the theorems with versions that take instance arguments though.

#### Kevin Buzzard (Sep 29 2018 at 13:36):

How big a project are we talking about? Have you checked https://github.com/leanprover-community/mathlib/wiki/Potential-projects for ideas?

Maybe a term, maybe a year, and no I didn't check that -- thanks!

#### Rob Lewis (Sep 29 2018 at 13:36):

@Kevin Buzzard We've had a few CS undergrads come to us looking for BS thesis projects and put together a short list for them. If you have students looking for projects more aligned toward programming/tactics than formalizing, we can share.

#### Mario Carneiro (Sep 29 2018 at 13:39):

By the way, that connectedness file finishes with a big TFAE proof

#### Johan Commelin (Sep 29 2018 at 14:21):

@Kevin Buzzard How about quadratic forms over Q? Maybe that is too big. But Hasse-Minkowski would be really cool. And we have QR now...

#### Johan Commelin (Sep 29 2018 at 14:22):

And p-adics, and Hensels lemma... so I think a lot of prerequisites are in place.

#### Patrick Massot (Sep 29 2018 at 14:54):

What about doing more elementary stuff?

#### Tobias Grosser (Sep 30 2018 at 15:11):

I am very interested in having functionality similar to: http://ssr.msr-inria.inria.fr/doc/mathcomp-1.5/MathComp.mxalgebra.html

Last updated: May 14 2021 at 20:13 UTC