Suggestions for maths/computing projects

Stream: maths

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

I think it should be generic in the type

[Kevin Buzzard]

I thought you had reservations about the Prime typeclass

[Kevin Buzzard]

On nat

[Mario Carneiro]

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

[Kevin Buzzard]

Is it ok if it's data?

[Mario Carneiro]

sure

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

is_of_nat?

[Kevin Buzzard]

math.nat?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

the_real_nat

[Mario Carneiro]

what about natural, integral etc?

[Mario Carneiro]

like "x is a natural element of A"

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

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]

But we need simply connected and path connected spaces first

[Mario Carneiro]

also connectedness

[Reid Barton]

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]

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

[Rob Lewis]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

and never really bothered to mention this to anyone

[Kevin Buzzard]

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

[Rob Lewis]

@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]

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]

@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]

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

[Johan Commelin]

@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]

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

[Patrick Massot]

What about doing more elementary stuff?

[Tobias Grosser]

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