Repo for the masterclass

Stream: Copenhagen Masterclass 2023

[Adam Topaz]

Hi all -- some of you may have already noticed that we made a dedicated github repo for next week's masterclass: https://github.com/adamtopaz/CopenhagenMasterclass2023

We will send invites to all the participants on the first day next week, but if you're already here and would like an invite, please let me know.

[Adam Topaz]

For some reason I tried to ping the stream with @stream but it seems I don't have the necessary permissions

[Adam Topaz]

I should also mention that the "schedule" on the README file is just a general guide, and may change especially later in the week depending on the participants' interest, etc.

There is a wiki page in this repo called "Topics". Please feel free to add things there! I hope there will be time to discuss those topics at least during the group-work/unstructured times in the afternoons.

[Dagur Asgeirsson]

I think there's an error in the installation instructions linked in the repo. Here: https://leanprover-community.github.io/install/macos.html it says to write

elan toolchain install stable
elan default stable

but stable is a lean 3 toolchain. It should be something like

elan toolchain install leanprover/lean4:nightly
elan default leanprover/lean4:nightly

right?

[Adam Topaz]

not only that, it also says to install mathlibtools, so that's definitely for lean3.

[Dagur Asgeirsson]

Right, I think you only need to install the VSCode lean 4 extension, and then write those two elan statements in the command line

[Dagur Asgeirsson]

Maybe also install elan

[Adam Topaz]

Well, as long as elan and the vscode extensions are installed, it should be okay to work with projects that already have a lean-toolchain file, so I think the current instructions will still suffice for the copenhagen repo.

[Dagur Asgeirsson]

Ah, so the lean-toolchain file installs the correct elan toolchain for you?

[Adam Topaz]

right. once you open a lean project in vscode, it looks for the lean-toolchain file and installs the version needed by the project if it's not already there.

[Adam Topaz]

@Dagur Ásgeirsson would you like to add "Solid abelian groups" to https://github.com/adamtopaz/CopenhagenMasterclass2023/wiki/Projects ?

[Dagur Asgeirsson]

Well I already have lots of lean 3 code for that, so it would be more of a porting project once we have the basics of condensed mathematics in mathlib 4

[Dagur Asgeirsson]

But it's easy to write down the definition once you have that limits exist in condensed abelian groups and the functor Profinite.{u} \func CondensedSet.{u}

[Dagur Asgeirsson]

In https://github.com/adamtopaz/CopenhagenMasterclass2023/blob/master/IDEAS.txt, I think
2) Example of {closed point, open point} showing set-theoretic issues? is irrelevant for us. The set theoretic issues are solved by universes in Lean.

[Patrick Massot]

Adam Topaz said:

not only that, it also says to install mathlibtools, so that's definitely for lean3.

Oh sorry, we missed that bit when updating the page.

[Mauricio Collares]

The OS X instructions also mention Rosetta, which shouldn't be needed for Lean 4 nightlies if I understand correctly

[Dagur Asgeirsson]

It's needed to install elan though, right?

[Mauricio Collares]

I don't think so, elan releases aarch64-darwin binaries: https://github.com/leanprover/elan/releases/tag/v1.4.6