Zulip Chat Archive

Stream: new members

Topic: jin.npc

jin.npc (Nov 20 2025 at 16:50):

Hello! I am a new member here (also the first time using Zulip). Very impressed by the amount of channels! I'd like to ask about where I can read the proof of that the LEAN's formal system is 'equally strong' as ZF+some axiom.. which channel should I ask?

Matthew Ballard (Nov 20 2025 at 16:52):

#leantt

jin.npc (Nov 20 2025 at 16:54):

Thank you @Matthew Ballard ! I will take a look at that paper. Could you also tell me where I can talk more about it in this zulipchat site?

Matthew Ballard (Nov 20 2025 at 16:55):

#Type theory is the general channel

Last updated: Dec 20 2025 at 21:32 UTC