Zulip Chat Archive

Stream: Lean for teaching

Topic: Kevin 2019

Patrick Massot (Oct 05 2019 at 10:08):

@Kevin Buzzard Do you want to tell us more about your Lean plans for 1st years undergrads? Do you need help with proofreading your documentation for students?

Kevin Buzzard (Oct 05 2019 at 10:13):

I'll answer at the end of this weekend. I want to see if I can get Bryan's fix for the sphinx issue working

Kevin Buzzard (Oct 05 2019 at 10:14):

As you might have spotted, there are unpolished drafts of things but I need to concentrate on my proper job right now, the lectures are more important than this lean thing :-/

Kevin Buzzard (Oct 10 2019 at 07:47):

http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

Kevin Buzzard (Oct 10 2019 at 07:47):

https://github.com/ImperialCollegeLondon/M40001_lean

Kevin Buzzard (Oct 10 2019 at 07:49):

That's what's "publically available" right now, although I haven't mentioned those links anywhere apart from here and to the Imperial students. Hmm. I can't change the name of this thread. I tried to change it to "Kevin teaching 2019" but failed

Last updated: Dec 20 2023 at 11:08 UTC