This week, we'll be doing a skillshare session on the programming language/proof assistant Lean. This skillshare workshop will be conducted by our regular member Johannes.
Content and format
The workshop will cover:
The Infoview, symbol input, basic mathematical syntax and proof
Namespaces and project organization
Working with `mathlib` and others, community resources and tutorials, `mathlib` nomenclature, tactics, and style
Autoformalization demo
The format of the workshop will be as a live demo by Johannes working through a learning repository for the workshop. At the start of the workshop, a GitHub link to the repo will be shared. Sufficient direction will be given in the repo so that you will be able to work through the repo alongside or in your own time. If you wish to follow along, visit https://lean-lang.org/install/manual/ to setup a Lean development environment in VS Code (we may be using Live Share, a VS Code only-extension, for the workshop).
Please remember to bring your own laptop or whatever device you set up the Lean development environment in.
Some level of mathematical maturity is required to get something out of the workshop; people who know lower undergrad level math should be able to follow along.
Location
Meet at Holland Village MRT Exit B (underground part) at 3 pm. We will wait for everyone to gather for 5-10 mins, and then head over to my nearby apartment. If you've been here before, feel free to come directly to the apartment (though you may need to wait to be let in).
Some snacks will be provided. There are many restaurants and a hawker centre nearby, if you want to buy your own food.
This week, we'll be doing a skillshare session on the programming language/proof assistant Lean. This skillshare workshop will be conducted by our regular member Johannes.
Content and format
The workshop will cover:
The format of the workshop will be as a live demo by Johannes working through a learning repository for the workshop. At the start of the workshop, a GitHub link to the repo will be shared. Sufficient direction will be given in the repo so that you will be able to work through the repo alongside or in your own time. If you wish to follow along, visit https://lean-lang.org/install/manual/ to setup a Lean development environment in VS Code (we may be using Live Share, a VS Code only-extension, for the workshop).
Please remember to bring your own laptop or whatever device you set up the Lean development environment in.
Some level of mathematical maturity is required to get something out of the workshop; people who know lower undergrad level math should be able to follow along.
Location
Meet at Holland Village MRT Exit B (underground part) at 3 pm. We will wait for everyone to gather for 5-10 mins, and then head over to my nearby apartment. If you've been here before, feel free to come directly to the apartment (though you may need to wait to be let in).
Some snacks will be provided. There are many restaurants and a hawker centre nearby, if you want to buy your own food.
Posted on: