Zulip Chat Archive
Stream: general
Topic: Mizar is open-source
Junyan Xu (Feb 26 2023 at 22:59):
Patrick Johnson said:
Unfortunately, metamath lacks automation and mizar is no longer actively developed (and more importantly not open source). I'm wondering what could be the reason there are no good set-theoretic theorem provers out there.
Mizar is open-sourced: http://mizar.uwb.edu.pl/forum/archive/2302/msg00001.html
(83.3k lines of Pascal)
Martin Dvořák (Feb 26 2023 at 23:45):
Junyan Xu said:
Mizar is open-sourced: http://mizar.uwb.edu.pl/forum/archive/2302/msg00001.html
(83.3k lines of Delphi(?) (GitHub says Pascal 100%))
Wow!
I just saw like 20 times more virtual methods in Pascal than I had seen over those years I programmed in Pascal.
Mario Carneiro (Feb 27 2023 at 01:29):
If you don't want to read those 80k lines of Pascal, then I have good news: I've been reimplementing Mizar in Rust: https://github.com/digama0/mizar-rs ! The details are in a just-submitted ITP paper which I will share here shortly, and it turned out to be just the right pressure to finally get Mizar to go full GPL.
Dean Young (Feb 27 2023 at 01:32):
Isabelle is nice. https://isabelle.zulipchat.com
Notification Bot (Feb 27 2023 at 01:56):
4 messages were moved here from #general > Opaque junk values for partial functions by Mario Carneiro.
Martin Dvořák (Feb 27 2023 at 07:25):
Mario Carneiro said:
If you don't want to read those 80k lines of Pascal, then I have good news: I've been reimplementing Mizar in Rust: https://github.com/digama0/mizar-rs ! The details are in a just-submitted ITP paper which I will share here shortly, and it turned out to be just the right pressure to finally get Mizar to go full GPL.
Wow! You do so many projects! How long did it take you to reïmplement Mizar in Rust?
Patrick Massot (Feb 27 2023 at 09:40):
Mario, could you comment on why you did that? Is the paper publicly available?
Johan Commelin (Feb 27 2023 at 09:41):
The details are in a just-submitted ITP paper which I will share here shortly
(Only meant to answer your 2nd question. I'm quite interested in an answer to Q1 as well.)
Mario Carneiro (Feb 27 2023 at 16:34):
This project is many years in the making, dating back even before I learned about lean. It finally got off the ground when I visited Josef Urban last summer and got the ball rolling on getting access to the source code. The project itself has been under active development for about four months. The main target is proof export from Mizar; I hinted at getting a crazy proof of the jordan curve theorem a while back and this is it
Mario Carneiro (Feb 27 2023 at 16:35):
Since Mizar is not a "small trusted core" style system, to get proofs from Mizar you basically have to do everything Mizar does, hence "reimplementation"
Matthew Ballard (Feb 27 2023 at 22:09):
This sounds like a nice hacker news post
Jireh Loreaux (Feb 27 2023 at 22:30):
Mario Carneiro said:
The main target is proof export from Mizar; I hinted at getting a crazy proof of the jordan curve theorem a while back and this is it
Are you suggesting you want to get a proof of the Jordan curve theorem in Lean by exporting a proof from Mizar? Surely I'm missing something, or else this is black magic.
Mario Carneiro (Feb 27 2023 at 22:30):
how so? I already did something like that for metamath
Mario Carneiro (Feb 27 2023 at 22:31):
Jireh Loreaux (Feb 27 2023 at 23:52):
I thought it would be harder for Mizar → Lean because of foundational clashes, or is this a "deep embedding" version of the Jordan curve theorem? I don't know much about these things, so I'm probably misunderstanding.
Mario Carneiro (Feb 28 2023 at 00:18):
foundational clashes are usually the least of your worries for this kind of thing
Mario Carneiro (Feb 28 2023 at 00:19):
like, worst case scenario you can add an axiom for the existence of some inaccessible cardinals
Jireh Loreaux (Feb 28 2023 at 00:49):
"foundational" was not the right word. I meant more, "how mathematical structures are represented in the system"
Last updated: Dec 20 2023 at 11:08 UTC