Lean Camp 2025 (general chat)

Stream: Berkeley Lean Seminar

[Jasper van de Kreeke]

Welcome! This is a test message for the Lean Camp 2025 general chat.

[Alok Singh]

Woah til there’s a lean camp

[Jasper van de Kreeke]

Yes, we're holding a Lean camp – warm-up sessions on Friday 13 + 20 June at 1pm in Evans Hall 891, and further weekly sessions throughout June–Aug. Thomas Browning and I are organizing it. This zulip channel will serve general communications. Everyone feel free to chip in.

[Kevin Buzzard]

Did this Berkeley lean camp get advertised in #announce or in a CA geographical channel? I went to a SF meet up and there were about ten people there (including Alok and Chris Bailey and Elliot Glaser from Epoch AI). There's an interesting group in the bay area

[Kevin Buzzard]

I should think that some people who are interested might not even know the existence of this channel

[Thomas Browning]

Yeah, I'll go ahead and post in geographic locality.

[Alok Singh]

Kevin Buzzard said:

Did this Berkeley lean camp get advertised in #announce or in a CA geographical channel? I went to a SF meet up and there were about ten people there (including Alok and Chris Bailey and Elliot Glaser from Epoch AI). There's an interesting group in the bay area

aww thanks @Kevin Buzzard

[Kevin Buzzard]

Also Robert Maxton was there and a bunch of people who may not be on the zulip

[Winston Yin (尹維晨)]

@Kevin Buzzard It’s a shame I missed out on meeting you in SF! Hope you enjoyed your time here.

[Manooshree Patel]

Jasper van de Kreeke said:

Yes, we're holding a Lean camp – warm-up sessions on Friday 13 + 20 June at 1pm in Evans Hall 891, and further weekly sessions throughout June–Aug. Thomas Browning and I are organizing it. This zulip channel will serve general communications. Everyone feel free to chip in.

Hello! I'm very excited about this camp, is there a sign-up for it?

[Thomas Browning]

Nope, just show up!

[Alok Singh]

Done for today?

[CJ Dowd]

I had trouble getting Mathematics In Lean to run on VS Code. On every file, my InfoView kept giving me the message "Imports are out of date and must be rebuilt; use the "Restart File" command in your editor" and then tried to redownload the entire mathlib when I restarted, even after having run
lake exe cache get.
I found the solution in this thread with Kevin Buzzard's "nuclear option".

[Thomas Browning]

The really nuclear option is just to delete your whole folder and re-clone the repo.

[Thomas Browning]

(at least, that's what I do whenever I get out of my depth)

[Ruslans]

Is the plan to continue meeting 1pm-3pm on Fridays?

[Jasper van de Kreeke]

Thanks for joining the first two sessions (warm-up) of the Lean Camp! We have a great crowd, last week Lucy and Manooshree already presented their own Lean (AI agent) projects. Fantastic! Last session we finished the natural number game, and starting from this week we will be continuing with Thomas Browning who will guide us to more advanced topics. The plan is to remain on Friday 1pm in Evans Hall 891. I'm looking forward to it!

[Alok Singh]

Jasper van de Kreeke said:

Thanks for joining the first two sessions (warm-up) of the Lean Camp! We have a great crowd, last week Lucy and Manooshree already presented their own Lean (AI agent) projects. Fantastic! Last session we finished the natural number game, and starting from this week we will be continuing with Thomas Browning who will guide us to more advanced topics. The plan is to remain on Friday 1pm in Evans Hall 891. I'm looking forward to it!

Can someone stream it so I may join along with a couple others in Boston? We’re from the bay but traveling.

[Seewoo Lee]

Jasper van de Kreeke 말함:

Thanks for joining the first two sessions (warm-up) of the Lean Camp! We have a great crowd, last week Lucy and Manooshree already presented their own Lean (AI agent) projects. Fantastic! Last session we finished the natural number game, and starting from this week we will be continuing with Thomas Browning who will guide us to more advanced topics. The plan is to remain on Friday 1pm in Evans Hall 891. I'm looking forward to it!

Are there any slides for the presentation?

[Jasper van de Kreeke]

Hi there! Thanks for writing. I'll try to make sure we stream via zoom on Friday. If there are any slides, I'll see whether we can share those via screen share. Enjoy!

[Thomas Browning]

Here's a zoom link: https://berkeley.zoom.us/j/91539414070

[Jasper van de Kreeke]

Rado Kirov said:

This might be an interesting set of exercises to do after the natural numbers game - https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/ (I haven't tried them)

Thanks, Rado!

[Jasper van de Kreeke]

Thanks everyone for joining today! Next week 4 July 1pm we will have a lightweight session for further practice.

[Rado Kirov]

Couldn't make it today because of work, but will try to stop by next Friday, since it is a holiday. The problems from Tao's analysis are pretty good so far - https://github.com/rkirov/analysis has my solutions for chapter 2 - modulo a few sorries in the epilogue, if someone can solve them, I would love to learn from them.

[Lucy Horowitz]

Are we meeting this week given July 4?

[Chris Bailey]

I think the conclusion was that there would be a "bonus session" on the 4th, maybe lighter fare or a little more of an open discussion.

[Jasper van de Kreeke]

Welcome everyone to today's session! Evans Hall is access restricted today because of 4 July. We likely need an arrangement to get some of us inside – One of us will be waiting around 1-1:10pm at the southwest entrance of Evans Hall (unless arranged otherwise). Good luck!

[Rado Kirov]

I came a bit late and outside by what I think is the southwest entrance

[Chris Bailey]

"The Filter game" for anyone who's interested (uses an old version of lean4, but elan will get it for you): https://github.com/bridgekat/filter-game

[Kevin Buzzard]

Note also secret filter game at https://adam.math.hhu.de/#/g/kbuzzard/FilterGame

[Kevin Buzzard]

written by me and a bunch of undergrads as a project, basically unfinished

[Patrick Massot]

Kevin, I think this is the same thing ported to Lean 4.

[Patrick Massot]

And let me add there is a lot of information about filters in #mil that didn’t exist at that time.

[Kevin Buzzard]

No it's not the same thing. Both of them were written under my supervision but they were different projects on the same topic. One was a second year undergraduate project, one was a summer school course. Someone should own this filter game project and turn it into a finished product.

[Jasper van de Kreeke]

Dear fellows, thanks again for your input! Based on what you've shared, Thomas and I have drafted a rough plan for the remaining ca. 8 sessions of the camp.

We're here to support, not prescribe, so the focus will soon shift to your own interests and ideas. We'll be organizing a brainstorming session where you can propose topics or results you'd like to formalize. From there, we’ll see where interests overlap and begin forming small project groups.

This transition could happen in a week or two, depending on how comfortable everyone feels moving beyond the tutorials. Until then, we’ll continue building Lean skills together as a group. Looking forward to what you'll create!

[Jasper van de Kreeke]

Dear all, this Friday we’ll begin working in small groups to pursue Lean projects during the remaining 7 sessions. Think about something you want to build – ambitious is good! Post ideas in this thread so others can join, combine, or be inspired.

[Sarayu Sirikonda]

Unfortunately, I won't be able to attend this week. Is there a zoom link to join online?

[Thomas Browning]

We can try using this link again: https://berkeley.zoom.us/j/91539414070

[Sarayu Sirikonda]

Thank you!

[Sarayu Sirikonda]

It says the meeting link is invalid

[Thomas Browning]

Try this one: https://berkeley.zoom.us/j/92943481474

[Jasper van de Kreeke]

Scoreboard is up! https://docs.google.com/spreadsheets/d/1OBznGv5Yh-71j5dSevxrsl5fwHl4CtTfGticftcE3f4/edit?gid=0#gid=0
Each week, fill in your team’s code size. The best team will win a prize at the end of camp. Also: keep defining what success looks like for you – when you want to hit what milestone. Individual achievements will be recognized too.

[Patrick A Carter]

Hi, I haven't been able to make it to these past two meetings. Will be back next week.

Was there a group working on a translation of Axler's LADR? I'd like to pivot to working on that if so. Would be great if someone could share info.

[Manooshree Patel]

Hi @Patrick A Carter I pitched working on LADR! I'll DM you

[Rado Kirov]

Is the camp meeting again this Friday? I can stop by again and share some of the solutions to Tao’s Real Analysis text I have been working on if that is of interest. Also would love to learn about creating a lean companion to LADR

[Thomas Browning]

Yup, we'll be meeting as usual 1pm-3pm (although I'll have to duck out around 2pm this week and next).

[Rado Kirov]

Something came up last minute, so I can't make it today :( In case anyone else is doing Tao's Analysis exercises my solutions are https://github.com/rkirov/analysis and I have chapter 2 and 3 done and happy to discuss solutions/problems, etc.

[Jasper van de Kreeke]

Everyone fill in your recent code size (no prize without filling out the scoreboard!). Thanks Michael for pointing out that edit access was missing.

[Jasper van de Kreeke]

Fellows – I’ve been put forward for the 2025 Postdoc Achievement Award, emphasizing my policy work for the Vice Chancellor of Research and other activities as VP of the Berkeley Postdoctoral Association. If you’d like to add a short supporting statement, that would be much appreciated. Attaching my CV for your reference.
cv.pdf

[Jasper van de Kreeke]

22 August will be our last session, before the semester starts. Chris Bailey will give us a surprise talk about the Lean kernel, but we'll make sure there's also time to finish any coding. After that we'll decide on prizes!

[Ching-Tsun Chou]

Would it be possible for those not in Berkeley to attend Chris Bailey's talk via Zoom?

[Chris Bailey]

Ching-Tsun Chou said:

Would it be possible for those not in Berkeley to attend Chris Bailey's talk via Zoom?

I can set something up. If there's anything in particular you'd like to see covered, let me know.

[Ching-Tsun Chou]

Thanks! Nothing in particular. I don't really know anything about Lean kernel.

[Jasper van de Kreeke]

Welcome! We are streaming Chris' talk on https://berkeley.zoom.us/meetings/8745936739/invitations?signature=cTu6I-PhUtq3r7cfMZ0JA4bBcDxKFMgKNzntnR-1Yzk

[Chris Bailey]

Switching to this google meet, sorry: https://meet.google.com/kgr-vbzd-zaz

[Ching-Tsun Chou]

Thanks for the talk! Are the presentation slides available online?

[Jasper van de Kreeke]

My pleasure to announce that Michael Kielstra is our winner for implementing convergence of the trapezoidal integration rule in Lean!