Zulip Chat Archive
Stream: general
Topic: livestream announcement
Kenny Lau (Jul 02 2020 at 06:54):
I am now live and I will try to prove that every polynomial splits in some bigger field.
Johan Commelin (Jul 02 2020 at 06:54):
We don't have that yet?
Kenny Lau (Jul 02 2020 at 06:55):
we're going to soon!
Johan Commelin (Jul 02 2020 at 06:55):
Aah, we only have adjoin_root
Markus Himmel (Jul 02 2020 at 06:55):
Where do we have to go to watch the stream?
Johan Commelin (Jul 02 2020 at 06:55):
discord of xena
Kenny Lau (Jul 02 2020 at 09:56):
The livestream has ended. Thank you for your participation.
Kevin Buzzard (Jul 02 2020 at 10:13):
And indeed now every polynomial does split in a bigger field. Johan and I heckled while Kenny coded. This is an interesting way of getting things done.
Scott Morrison (Jul 02 2020 at 10:31):
It will be so exciting if we can get Live Share working with VS Code. Then the person being heckled can sorry a side goal and say "shut up and fix that sorry for me, Kevin" :-)
Kevin Buzzard (Jul 02 2020 at 10:37):
Lean Live Share coding would be super-helpful for me right now; training people remotely is much harder than looking over their shoulder. If they're working on one file then they can cut and paste it, and then we hope that their mathlib is approximately the same as mine (which is not always true, stuff moves so fast nowadays :-) ). If they're doing something more substantial, or if things just aren't working, then just leaping in and fixing stuff would be brilliant.
Patrick Massot (Jul 02 2020 at 12:05):
Did you try CoCalc?
Johan Commelin (Jul 02 2020 at 12:53):
But with CoCalc it's hard to get up-to-date mathlib, right?
Kevin Buzzard (Jul 02 2020 at 13:10):
It's impossible, now Lean started moving again. They can't keep up with Lean
Johan Commelin (Jul 02 2020 at 13:11):
Sure, I understand this
Mario Carneiro (Jul 02 2020 at 13:12):
How good is Cocalc support for local lean installs?
Kenny Lau (Jul 02 2020 at 13:13):
can't we just tell cocalc to leanproject up?
Mario Carneiro (Jul 02 2020 at 13:14):
you still need to get your local lean to run as the server when you open a lean file
Mario Carneiro (Jul 02 2020 at 13:14):
the server that normally runs is in some global .elan directory that you can't touch
Mario Carneiro (Jul 02 2020 at 13:16):
It should be possible to have that directory contain every lean version ever and then leanproject up should work, but it would still require either prodding the cocalc team to update every time a new lean version comes out (which is often) or somehow getting them to entrust us maintainers with upload capabilities (unlikely)
Rob Lewis (Jul 02 2020 at 13:43):
I'm pretty sure you have enough permission as a CoCalc user to replace the default installation with whatever setup you want (and the editor wll pick up on this). The problems are (1) you'd have to somehow distribute these changes to other CoCalc users if you want them to have the same setup as you; (2) free CoCalc accounts can't access the internet directly, so for those, you'd need to manually upload whatever files you need and then place them.
Rob Lewis (Jul 02 2020 at 13:43):
(2) gets in the way of leanproject big time.
Kevin Buzzard (Jul 02 2020 at 21:22):
I have a paid CoCalc account. I have certainly used my own choice of mathlib on CoCalc but I've never used my own choice of Lean
Kenny Lau (Jul 03 2020 at 12:42):
I am now live and I will try to construct a splitting field using a different approach.
Chris Hughes (Jul 03 2020 at 13:23):
I do have some old code where I construct a splitting field. You're welcome to fix that and PR it if you want.
Kenny Lau (Jul 03 2020 at 13:59):
Now I am trying to implement algebra towers.
Kenny Lau (Jul 03 2020 at 18:06):
The livestream has ended. Thank you for your participation.
Kenny Lau (Aug 04 2020 at 05:32):
30 minutes from now, to experiment with composable morphisms
Bolton Bailey (Sep 13 2025 at 20:41):
At around 5pm pacific time tonight I’m going to livestream my attempt at proving one of the lemmas from the AKS primality test paper, stay tuned for more info.
Bolton Bailey (Sep 13 2025 at 20:43):
Bolton Bailey (Sep 13 2025 at 23:57):
Here is a link https://www.youtube.com/watch?v=4Vf7d_GrW7A
(and now here is a VOD)
Bolton Bailey (Sep 14 2025 at 02:16):
Thanks everyone for joining, I didn't get very far :sad: hopefully I can come back and do more later.
Aaron Liu (Sep 14 2025 at 02:18):
Bolton Bailey said:
Thanks everyone for joining, I didn't get very far :sad: hopefully I can come back and do more later.
it was very painful to watch because I had solutions to all your problems
Alfredo Moreira-Rosa (Sep 14 2025 at 02:47):
it's not very nice to say that. You could give positive feedback and still be constructive.
Kevin Buzzard (Sep 14 2025 at 11:01):
When I was livestreaming in the past I would have people making suggestions in the comments, and these were very much appreciated.
Aaron Liu (Sep 14 2025 at 11:02):
Kevin Buzzard said:
When I was livestreaming in the past I would have people making suggestions in the comments, and these were very much appreciated.
unfortunately I can't make comments without being signed in to youtube :(
Kevin Buzzard (Sep 14 2025 at 11:25):
Oh so then it sounds like your pain is a you problem, not Bolton's problem!
Arthur Paulino (Sep 15 2025 at 12:44):
Aaron Liu said:
it was very painful to watch because I had solutions to all your problems
Please don't discourage anyone taking the initiative. This has a cascading effect of discouraging others that might be considering to livestream Lean 4 too.
Aaron Liu (Sep 15 2025 at 15:35):
Arthur Paulino said:
Aaron Liu said:
it was very painful to watch because I had solutions to all your problems
Please don't discourage anyone taking the initiative. This has a cascading effect of discouraging others that might be considering to livestream Lean 4 too.
Sorry I wasn't trying to be discouraging. I was just commenting on the experience. If this is bad I won't do it in the future.
Patrick Massot (Sep 15 2025 at 21:26):
I read Aaron’s comment as: “it was very painful because I wanted to help but couldn’t”. Am I misunderstanding?
Aaron Liu (Sep 15 2025 at 21:32):
Patrick Massot said:
I read Aaron’s comment as: “it was very painful because I wanted to help but couldn’t”. Am I misunderstanding?
that was roughly my intention, and I didn't mean to be discouraging
Arthur Paulino (Sep 15 2025 at 21:37):
Communication noise :sad:...
Btw, thanks a lot Aaron. You're certainly super helpful. Your comments somehow get to the core of the issues
Weiyi Wang (Sep 15 2025 at 21:51):
We have chat backseating in Lean now /s
Bolton Bailey (Sep 15 2025 at 23:18):
Aaron Liu said:
Patrick Massot said:
I read Aaron’s comment as: “it was very painful because I wanted to help but couldn’t”. Am I misunderstanding?
that was roughly my intention, and I didn't mean to be discouraging
No worries, I didn't take the comment amiss.
Bolton Bailey (Sep 15 2025 at 23:20):
I'm going to pick back up tomorrow, so feel free to join again.
Actually seems I have a dentist appointment then, so I'll change it to
Bolton Bailey (Sep 17 2025 at 20:01):
Here is a link https://www.youtube.com/watch?v=wOpnyFulNJ4
And here is a video trimmed for dead air https://youtu.be/oIKznqaGmzs
Malvin Gattinger (Sep 17 2025 at 20:14):
Thanks for doing this, I have no clue about what you are proving but already learned something from watching, namely to use quotes to actually find stuff on loogle :-) (Also, I don't want to log in to youtube so I am wondering if chatting here is also okay?)
Violeta Hernández (Sep 17 2025 at 20:59):
Unfortunately can't join atm, but I've subscribed so I don't miss the next one :slight_smile:
Ilmārs Cīrulis (Sep 17 2025 at 21:00):
Is the chat working for those who are logged into Youtube?
Bolton Bailey (Sep 17 2025 at 21:15):
Looks like they aren't, sorry! Not sure what the issue is, but people can comment here.
Aaron Liu (Sep 17 2025 at 21:26):
really? isn't this an announcement thread?
Bolton Bailey (Sep 17 2025 at 21:30):
Ok, yes, maybe that's a good point
Bolton Bailey (Sep 17 2025 at 21:31):
Actually seems Rida managed to comment, so maybe I am mistaken about it not being possible to comment on the YT chat.
Bolton Bailey (Sep 17 2025 at 22:21):
Ok that's it for today, maybe for future reference when a livestream is made there can be a separate day-specific thread made for live Zulip comments, as is typically done in the #announce channel
Bolton Bailey (Sep 19 2025 at 16:04):
Ok, late notice but I have some more time in my schedule so I'm going to get back on this in ten minutes or so. I have recently been trying to use github copilot to work on some other problems, so I'm going to try that out here today, I think.
Bolton Bailey (Sep 19 2025 at 16:15):
Link here https://www.youtube.com/watch?v=gQ-QnsBJU6M
If anyone has no youtube account, feel free to link to another thread from here and give comments on Zulip
Bolton Bailey (Sep 19 2025 at 19:05):
Here is the uploaded shortened version, thanks again to everyone who came and gave me pointers!
Snir Broshi (Sep 21 2025 at 06:51):
Apparently the limit of (LCM n) ^ (1 / n : ℝ) is e, could be cool to prove it too (I have no idea how hard it is compared to the lower bound)
Michael Stoll (Sep 21 2025 at 08:35):
This is equivalent to the Prime Number Theorem: if you take the log and use the definition of LCM n, the expression becomes the average of the von Mangoldt function from 1 up to n, and one version of PNT (the version that is in fact easiest to prove) says that the summatory function of the von Mangoldt function is asymptotic to n.
l1mey (Dec 16 2025 at 20:07):
In about 2 hours, I'm going to livestream my first Lean project which is formalising LLVM style undefined behaviour and proving some compiler optimisations from that.
https://l-m.dev/stream/1765922400
https://www.twitch.tv/lmdotdev/
Last updated: Dec 20 2025 at 21:32 UTC