Zulip Chat Archive

Stream: maths

Topic: Suggestions for maths/computing projects


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 11:59):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 12:02):

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

view this post on Zulip Mario Carneiro (Sep 29 2018 at 12:02):

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

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 12:03):

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

view this post on Zulip Mario Carneiro (Sep 29 2018 at 12:03):

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

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 12:04):

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

view this post on Zulip Mario Carneiro (Sep 29 2018 at 12:04):

I think it should be generic in the type

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 12:04):

I thought you had reservations about the Prime typeclass

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 12:04):

On nat

view this post on Zulip Mario Carneiro (Sep 29 2018 at 12:05):

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

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 12:05):

Is it ok if it's data?

view this post on Zulip Mario Carneiro (Sep 29 2018 at 12:05):

sure

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 29 2018 at 12:06):

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

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 12:06):

is_of_nat?

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 12:07):

math.nat?

view this post on Zulip Mario Carneiro (Sep 29 2018 at 12:08):

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

view this post on Zulip Mario Carneiro (Sep 29 2018 at 12:08):

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

view this post on Zulip Mario Carneiro (Sep 29 2018 at 12:09):

the_real_nat

view this post on Zulip Mario Carneiro (Sep 29 2018 at 12:09):

what about natural, integral etc?

view this post on Zulip Mario Carneiro (Sep 29 2018 at 12:10):

like "x is a natural element of A"

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 29 2018 at 13:06):

But we need simply connected and path connected spaces first

view this post on Zulip Mario Carneiro (Sep 29 2018 at 13:06):

also connectedness

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 29 2018 at 13:30):

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

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 13:32):

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

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 13:32):

and never really bothered to mention this to anyone

view this post on Zulip Kevin Buzzard (Sep 29 2018 at 13:32):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 29 2018 at 13:39):

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

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Sep 29 2018 at 14:22):

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

view this post on Zulip Patrick Massot (Sep 29 2018 at 14:54):

What about doing more elementary stuff?

view this post on Zulip 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