Zulip Chat Archive

Stream: maths

Topic: squeeze_ring


view this post on Zulip Kevin Buzzard (Apr 08 2020 at 18:27):

So I am very pleased to see that nobody other than @Kenny Lau can do the codewars Kata about proving that no commutative ring has 5 units. I wrote a proof which compiles fine but takes around 10 seconds on my machine, which is too long for the codewars servers. In short, I have to optimise my code. One way of perhaps saving some time would be to replace all occurrences of ring or ring_exp with an explicit list of rewrites :-) I have absolutely no idea how close to being possible that is :-)

view this post on Zulip Alex J. Best (Apr 08 2020 at 18:28):

Hey, I can do it!! My proof is just over 16000 ms :frown: :anguish:

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 18:29):

Yeah, you can "do" it like I can do it, i.e. it times out :-)

Try submitting it 100 times and see if you get lucky? :-)

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 18:30):

Gratz on the maths proof, by the way! It's tricky to formalise in Lean!

view this post on Zulip Alex J. Best (Apr 08 2020 at 18:30):

Yes I've tried! but no luck so far, maybe I should find a time of the night the codewars servers are least loaded?

view this post on Zulip Alex J. Best (Apr 08 2020 at 18:31):

Yeah it was a fun problem so thanks to you both for putting it up! And for everyone who got codewars running in the first place!

view this post on Zulip orlando (Apr 08 2020 at 19:09):

@Kevin Buzzard You show that if GG is a group and Card(G)4 \text{Card}(G) \leq 4 then GG is commutative ?

view this post on Zulip orlando (Apr 08 2020 at 19:10):

hum i missread ! :confused:

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 19:12):

The lemma is that no RR has R×=5|R^\times|=5

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 19:13):

although that looks like another fabulous kata :-)

view this post on Zulip Kenny Lau (Apr 08 2020 at 19:14):

it follows from p is commutative and p^2 is commutative

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 19:14):

Do we have that in Lean?

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 19:14):

and anyway, you missed out the case p0p^0

view this post on Zulip Kenny Lau (Apr 08 2020 at 19:14):

the case for 1 is a bunch of subsingleton elim

view this post on Zulip Kenny Lau (Apr 08 2020 at 19:14):

maybe we can have a kata proving p^2 is commutative

view this post on Zulip Kenny Lau (Apr 08 2020 at 19:15):

and if we go on we'll recreate @Chris Hughes' Sylow's theorems

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 19:15):

aah, any group of order p0p^0 embeds in a group of size p1p^1 so it follows from the p1p^1 case.

view this post on Zulip Kenny Lau (Apr 08 2020 at 19:16):

sorry you already used subsingleton


Last updated: May 14 2021 at 19:21 UTC