Glimpse of Lean Intuitionistic logic

Stream: new members

[Thomas Vigouroux]

Hey there, I was going through the Intuitionistic proposition logic in Glimsp of lean, and got to the end.

From there, I would like to continue and prove completeness of the natural deduction we have formalized with regard to Heyting semantics, but I can't find any resources on the subject (so that I can slowly get started).

Is there something somewhere ?

[chenjulang]

check this out : https://leanprover-community.github.io/learn.html

[chenjulang]

the game link : https://adam.math.hhu.de/#/g/hhu-adam/NNG4
and the solutions : https://github.com/ImperialCollegeLondon/natural_number_game

[Thomas Vigouroux]

Hmmm, I don't think I made my question clear enough

[Thomas Vigouroux]

I am specifically searching for ressources about Natural deduction in intuitionistic logic, and completeness with regard to heyting semantics

[Julian Berman]

I don't know what any of these things are, so apologies if I too don't give you anything useful, but a few experts I know have muted this stream given it's generally for newer user questions -- you may have more luck asking that in #Is there code for X? if you can make some statement precise (i.e. write a lean type probably) or else maybe #Type theory perhaps (assuming I'm even guessing the subfield correctly)?

[Thomas Vigouroux]

Oh okay, will do then !

[Thomas Vigouroux]

I made good progress in the proof, and I think that the remaining cases are fairly trivial, would anyone be interested in seeing (and critiquing) the proof resulting from that ?

[Thomas Vigouroux]

I only had to change from Set Formula to Finset Formula which seems reasonnable to me (and otherwise I simply could not prove anything).

[James Wiles]

Are there any good YouTube videos working through the Glimpse of Lean repo? https://github.com/PatrickMassot/GlimpseOfLean