Stream: new members
jachym simon (Nov 16 2020 at 17:10):
Hello! I was formalising a proof of completeness and soundness of classical propositional logic and i managed succesfuly (did that as a bachelor thesis). I wanted to ask, whether it has some actual value, can be used somewhere or something? I kind of suppose its nothing complicated (maybe it was even done before?), but still. I also would be very thankful- since i am fairly bad with lean and not at all sure with what i created- if someone would be up for scanning through the code to give me some feedback. Its approximately 800 lines long. Cheers, Jachym
Johan Commelin (Nov 16 2020 at 17:15):
Congrats on completing your project!
I don't know anything about logic, but I'm sure it doesn't hurt if you paste a link to your code here.
jachym simon (Nov 16 2020 at 17:24):
Thank you :)
True, I will upload it and paste the link here.
Jasmin Blanchette (Nov 16 2020 at 17:37):
It has been done before in other systems -- see e.g. https://www21.in.tum.de/~nipkow/pubs/types17.pdf . It's always interesting to have these proofs in Lean.
jachym simon (Nov 19 2020 at 16:39):
Sooo... i wasnt sure how to share it, so i tried to put it up on github. Here is the link (i hope it works, i dont have much experience with github). Any feedback will be much appreciated!
Last updated: May 12 2021 at 03:23 UTC