Hi all, How delightful to see our tiny project find its way onto your mailing list! I am one of the developers for Metamathix (Arthur Correnson <[email protected]> being the other). The project is at its infancy, but we already have a minimal implementation of a proof checker (without parsing/output) that we hope to prove correct with respect to a declarative specification or formal semantics for Metamath's underlying logic. To this end, if there already exists a reasonable model for Metamath then we'd love to hear about it. At present, we have proposed a reference logic and semantics, but we are rather unsure if they make sense.
Looking forward to hearing your thoughts, Denis On Monday, February 27, 2023 at 10:58:04 AM UTC+1 Thierry Arnoux wrote: > Hi David, > > Feel free to add it! > > > On 26/02/2023 16:20, David A. Wheeler wrote: > > We have a list of Metamath tools on the website pages. Will you add it? If > not, let me know and I will add it, I just don't want to duplicate effort. > > On February 25, 2023 3:26:02 PM EST, Thierry Arnoux <[email protected]> > wrote: >> >> Hi all, >> >> FYI, I recently found out about Metamatix >> <https://github.com/acorrenson/metamatix>, a verified implementation of >> a metamath proof checker, written in Coq. >> >> I'm not sure how far the project goes, but it's probably of interest for >> people in this group. >> >> BR, >> _ >> Thierry >> > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/5DBFBC50-D236-4A71-9F55-82392C457A1A%40dwheeler.com > > <https://groups.google.com/d/msgid/metamath/5DBFBC50-D236-4A71-9F55-82392C457A1A%40dwheeler.com?utm_medium=email&utm_source=footer> > . > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/eaea1b13-6b52-4a1f-87a1-1f2d007d08dfn%40googlegroups.com.
