NF consistency verification

Stream: general

[Michael Beeson]

It has been announced that the Lean verification of Randall Holmes's consistency proof of New Foundations set theory has been completed. Where can I get the Lean files?

[Kim Morrison]

@Michael Beeson, please see https://github.com/leanprover-community/con-nf

[Michael Beeson]

OK, I cloned the repository and tried to open it in Visual Studio Code, but there's no leanpkg.toml file. Um, I know that a .toml file is needed, but I forget how to make one or get one...

[Michael Beeson]

Never mind, I had to install the Lean 4 extension to VS code, that was all.

[Kim Morrison]

leanpkg.toml is a Lean 3 thing --- now you're expecting to see either a lakefile.lean or (very new!) lakefile.toml.