Great talk Mario! Thanks for sharing.
I nearly asked a couple of nights ago when it turned out Glauco and I have
both accidentally written Metamath verifiers in TypeScript which probably
run in O(n^2), hopefully on our way to writing verifiers that are actually
useable! What's a 'good' length of time in big-O notation for a verifier
to run in?
In your talk you state that this is O(n) - unless I've wildly misunderstood.
I'm pleasantly surprised by that, and also curious. The best I was hoping
for was O(n.log(n)), and my thinking was that as you add more proofs to the
system, subsequent proofs sometimes refer back to them, which requires the
verifier to do a look up, which is why I was assuming 'n' to make your pass
of the file, and 'log(n)' for the lookups. Broadly, how does an O(n)
verifier avoid the need for this, please?
Best regards,
Antony
On Wed, May 11, 2022 at 11:03 AM Mario Carneiro <[email protected]> wrote:
> Hi all,
>
> I finally put the recording of my talk "Lessons from Metamath" from the
> Lorentz Center meeting for Machine-Checked Mathematics on YouTube. It is
> primarily aimed at an audience of people who are familiar with proof
> assistants but not with Metamath, but I'm sure you all can get plenty out
> of it as well.
>
> https://www.youtube.com/watch?v=OOF4NWRyue4
>
> Mario Carneiro
>
> --
> 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/CAFXXJSsoNfduP5TgNbDzPMQEfFYYc4aCRt0y2aPRFPn6sH8ZyQ%40mail.gmail.com
> <https://groups.google.com/d/msgid/metamath/CAFXXJSsoNfduP5TgNbDzPMQEfFYYc4aCRt0y2aPRFPn6sH8ZyQ%40mail.gmail.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/CAJ48g%2BCwN2q7qKqi5oh4WezRV75V%2BikgT9DJyT4_tbmO825yyQ%40mail.gmail.com.
