Lean at Duke

Stream: Lean for teaching

[Patrick Massot]

A colleague pointed out https://momath.org/qed/ which will happen tonight. @Colleen Robles, is there anything public about your work?

[Colleen Robles]

Hi @Patrick Massot The project was part of Duke's Math+ program
https://math.duke.edu/mathplus/2023
which provides team-based, summer research projects for undergraduates. You can find more about the team's work at
https://math.duke.edu/mathplus/2023/automated-theorem-proving-and-proof-verification
And the Linear Algebra Game the developed (based on the blueprint provided by Buzzard and Pedramfar's Natural Number Game) is publicly available at
https://stavan-jain.github.io/linear_algebra_game/
This is very much the work of the team (Yannan Bai, Annapurna Bhattacharya, Stavan Jain, Kurt Ma, Ricardo Prado Cunha, Anoushka Sinha), my involvement was minimal.

[Kevin Buzzard]

@Colleen Robles the hard work with these games is organising the material into a reasonable order. Porting the game to Lean 4 should be easy in comparison :-)

[Colleen Robles]

Kevin Buzzard said:

Colleen Robles the hard work with these games is organising the material into a reasonable order. Porting the game to Lean 4 should be easy in comparison :-)

@Kevin Buzzard That is great to hear. I'm planning another project next summer and anticipate using Lean 4. Will there be a tutorial available by then?

[Patrick Massot]

Thanks! It looks very nice. Are you aware of anyone interested in porting this to Lean 4?

[Kevin Buzzard]

The Lean 4 version of the natural number game is in progress here https://github.com/hhu-adam/NNG4 and I just read this to figure out how to use it. You can see what the Lean 4 version of the game looks like here but within a few weeks there will be a bunch of new stuff on that page.

[Patrick Massot]

Also note that the Lean 4 game interface is currently work in progress. Soon it will be even more beautiful and convenient.

[Colleen Robles]

Patrick Massot said:

Thanks! It looks very nice. Are you aware of anyone interested in porting this to Lean 4?

No, I'm not aware of anyone at this time. But if I supervise another Lean-based project next summer, this would be one possibility for the work.

[Patrick Massot]

Would you be open to seeing someone else doing it in the mean time? Note that I'm not suggesting I would do it. But maybe people from the Adam project would be happy to have one more game available on their platform @Jon Eugster @Alexander Bentkamp

[Colleen Robles]

Patrick Massot said:

Would you be open to seeing someone else doing it in the mean time? Note that I'm not suggesting I would do it. But maybe people from the Adam project would be happy to have one more game available on their platform Jon Eugster Alexander Bentkamp

Absolutely! And if someone does work on it, let me know. I'll be interested to hear how it goes.

[Mac Malone]

Colleen Robles said:

The project was part of Duke's Math+ program
https://math.duke.edu/mathplus/2023
which provides team-based, summer research projects for undergraduates. You can find more about the team's work at
https://math.duke.edu/mathplus/2023/automated-theorem-proving-and-proof-verification
And the Linear Algebra Game the developed (based on the blueprint provided by Buzzard and Pedramfar's Natural Number Game) is publicly available at
https://stavan-jain.github.io/linear_algebra_game/
This is very much the work of the team (Yannan Bai, Annapurna Bhattacharya, Stavan Jain, Kurt Ma, Ricardo Prado Cunha, Anoushka Sinha), my involvement was minimal.

Very cool! I was not aware there was anyone else in North Carolina actively working with Lean, especially within the Research Triangle area (and present on this Zulip)!

[Mac Malone]

I guess I had missed you @Colleen Robles

[Mac Malone]

(Maybe I should have searched the #Geographic locality stream more carefully)

[Jon Eugster]

Yes we would indeed be happy to see more lean4-games, and while the doc isnt perfect yet, Im happy to have the docs improved whenever somebody new plans to use it (or make up for the missing doc by direct support)

No promise, but maybe I'll find time to translate your game to Lean 4 over the next months

[Ricardo Prado Cunha]

I'm one of the students that worked on the the linear algebra game. While we did consider using Lean4, the base we were building on from the natural number game was in Lean3 and we didn't have much experience with Lean in the browser (I spent several hours figuring out how to update the version of lean3 that is used by lean-game-maker), so we thought it would be best to stick with Lean3.
That said, from my experience with Lean4 in making a PR to mathlib4 (sorry about not finishing the docs for that yet), it does seem nice and I think that its syntax would be easier for students than Lean3's syntax since it is closer to Python's syntax. At this time I am quite busy so I wouldn't take up the project myself, but if someone else starts it I would be interested in contributing.