That sounds awesome. I'd be interested in reading your thesis when you're done, if that's ok, which I hope feels cool as often it's a struggle to even get the committee to read it haha. And yeah looking forward to seeing where you take the system, I think it's got a lot of power and once MM0 is checked in MMC that's a really solid basis I think.
On Wednesday, May 18, 2022 at 4:32:20 PM UTC+1 [email protected] wrote: > On Wed, May 18, 2022 at 11:24 AM Jon P <[email protected]> wrote: > >> Is it ok to ask about your progress on MM0/MM1? Where have you got to >> with it, what have you been working on recently and where are you hoping to >> get to with it? I think it's awesome what you're doing with it and I'm >> interested to see what becomes of it. (I guess maybe this should be a new >> thread but I thought I would ask here). >> > > I'm currently in the final stages of the PhD, so in a few weeks I will > basically have a whole book about MM0. That's what has been occupying me of > late. Once the deadlines for that are passed, I will probably go back to > working on the MMC compiler lemmas with the goal of making the verifying > compiler actually produce full correctness theorems, and then start growing > the set of operations that the programming language supports and handle all > the trivial bugs that I have noticed while writing about it. > > After that comes the implementation of the MM0 verifier in MMC, and then > adding all the invariants and proving them, and then it will actually be a > bootstrapping system as originally intended. > > >> >> On Thursday, May 12, 2022 at 3:39:03 PM UTC+1 [email protected] wrote: >> >>> Correction: There was a bug in the code that lead to unusually large >>> values for "avg score", due to a single very large data point. The >>> corrected results: >>> >>> avg score: 75178012 / 3075357 = 24.4 >>> avg lg(score): 10750001.8 / 3075357) = 3.4955 = lg(11.2787) >>> avg sqrt(score): 12640434.2 / 3075357 = 4.1102 = sqrt(16.8940) >>> >>> shuffled 1: >>> avg score: 157481709 / 3075357 = 51.2 >>> avg lg(score): 12857460.5 / 3075357) = 4.1808 = lg(18.1362) >>> avg sqrt(score): 17549817.2 / 3075357 = 5.7066 = sqrt(32.5652) >>> >>> shuffled 2: >>> avg score: 157220284 / 3075357 = 51.1 >>> avg lg(score): 12861417.8 / 3075357) = 4.1821 = lg(18.1524) >>> avg sqrt(score): 17552661.4 / 3075357 = 5.7075 = sqrt(32.5758) >>> >>> completely random 1: >>> avg score: 565223103 / 3075357 = 183.8 >>> avg lg(score): 22394511.3 / 3075357) = 7.2819 = lg(155.6242) >>> avg sqrt(score): 40151474.7 / 3075357 = 13.0559 = sqrt(170.4559) >>> >>> completely random 2: >>> avg score: 565104301 / 3075357 = 183.8 >>> avg lg(score): 22394838.4 / 3075357) = 7.2820 = lg(155.6357) >>> avg sqrt(score): 40149999.7 / 3075357 = 13.0554 = sqrt(170.4433) >>> >>> On Thu, May 12, 2022 at 9:36 AM Mario Carneiro <[email protected]> wrote: >>> >>>> I got curious about this, so here's some code to do just that. We can >>>> calculate the "unified bound" ( >>>> https://www.youtube.com/watch?v=DZ7jt1F8KKw&t=1178s) explicitly for >>>> the access sequence used in set.mm using some stuff on top of >>>> metamath-knife (code here: >>>> https://gist.github.com/digama0/78c5a2de9589d53b4667b9a75b3ca5f3), and >>>> the result is: >>>> >>>> Define the score of an access x_j to be the min of (t_ij + |x_i - x_j|) >>>> over all previous x_i in the sequence, where t_ij is the number of >>>> distinct >>>> values in {x_i, ..., x_j-1}. Then we can compute the average score of the >>>> access sequence, for different kinds of average weighting: >>>> >>>> set.mm commit 3de3ae52 >>>> number of theorems: 42879 >>>> >>>> avg score: 4370145307 / 3075357 = 1421.0 >>>> 2^(avg log(score)): 2^(10750033.8 / 3075357) = 2^3.4955 = 11.2788 >>>> (avg sqrt(score))^2: (12705970.2 / 3075357)^2 = 4.1315^2 = 17.0696 >>>> >>>> shuffled 1: >>>> avg score: 4452015191 <(445)%20201-5191> / 3075357 = 1447.6 >>>> 2^(avg log(score)): 2^(12857388.6 / 3075357) = 2^4.1808 = 18.1359 >>>> (avg sqrt(score))^2: (17604771.6 / 3075357)^2 = 5.7245^2 = 32.7695 >>>> >>>> shuffled 2: >>>> avg score: 4453096882 <(445)%20309-6882> / 3075357 = 1448.0 >>>> 2^(avg log(score)): 2^(12873701.1 / 3075357) = 2^4.1861 = 18.2027 >>>> (avg sqrt(score))^2: (17659385.1 / 3075357)^2 = 5.7422^2 = 32.9731 >>>> >>>> completely random 1: >>>> avg score: 4860210535 / 3075357 = 1580.4 >>>> 2^(avg log(score)): 2^(22395391.0 / 3075357) = 2^7.2822 = 155.6550 >>>> (avg sqrt(score))^2: (40220315.5 / 3075357)^2 = 13.0783^2 = 171.0409 >>>> >>>> completely random 2: >>>> avg score: 4860319828 / 3075357 = 1580.4 >>>> 2^(avg log(score)): 2^(22396702.0 / 3075357) = 2^7.2826 = 155.7010 >>>> (avg sqrt(score))^2: (40224473.6 / 3075357)^2 = 13.0796^2 = 171.0762 >>>> >>>> That is: the log-weighted average of the scores is 11.2, meaning that >>>> the s in O(n log(s)) is 11.2 and log(s) is about 3.49. To get a sense for >>>> how good spatial layout in set.mm is, I compare this to a randomized >>>> layout (I didn't pay attention to dependency order here, it's just a >>>> shuffle), which results in 18.1 for s. To double check the variance on the >>>> random layout calculation I ran it twice and you can see the second result >>>> is almost the same, 18.2, so clearly set.mm is laid out much better >>>> than random. >>>> >>>> Note that this shuffle simulation does not account for the difference >>>> in temporal locality: I am still simulating the same accesses in the same >>>> order, even though they would presumably be done in the same random order >>>> used for the layout. This is probably not a big effect since this only >>>> affects ordering between proofs: most of those 3 million accesses occur >>>> (there are only around 65000 theorems in the set) because one proof >>>> involves many accesses, so the majority of temporal locality would not be >>>> affected by reshuffling theorems. >>>> >>>> The "completely random" data just uses the output of a random number >>>> generator with the same range and length as the set.mm access >>>> sequence. The value of s is now much larger, 155.7. I believe the >>>> operative >>>> effect here is the within-proof locality: the same theorems are referenced >>>> many times in a given proof, while a random proof will touch a lot more of >>>> the library. >>>> >>>> All in all I would say this is a pretty small number: s = 11.2 is very >>>> far from n = 3075357, so even if it's not constant (obviously difficult to >>>> measure) it is still very sub-linear. >>>> >>>> On Thu, May 12, 2022 at 6:35 AM Thierry Arnoux <[email protected]> >>>> wrote: >>>> >>>>> Rather than shuffling which sounds complex, a simpler way to verify >>>>> that hypothesis might be to count the number of different >>>>> chapters/sections >>>>> each theorem uses, and have a statistical approach to confirm whether >>>>> that >>>>> matches with O(1) as Mario suggests. >>>>> >>>>> On 12/05/2022 18:04, Mario Carneiro wrote: >>>>> >>>>> It's tricky to shuffle an mm file because theorem dependencies put a >>>>> constraint on allowable reorderings. I would probably do a random shuffle >>>>> and then do DFS to get a topological ordering in order to get a random >>>>> allowable ordering. >>>>> >>>>> My prediction would be that it does not make a huge effect on >>>>> verification speed. Except for the most optimized, Metamath verifiers are >>>>> typically bottlenecked on things other than loading the theorem into >>>>> cache; >>>>> stuff like substituting expressions into theorem statement are probably >>>>> 20-100 times more expensive except at *really* large scale. >>>>> >>>>> On Thu, May 12, 2022 at 5:24 AM Antony Bartlett <[email protected]> >>>>> wrote: >>>>> >>>>>> Wow, great answer, thanks Mario! Mind duly blown. >>>>>> >>>>>> The claim that contributors to mm files have in effect sorted the >>>>>> proofs in a manner favorable to efficient verification should be >>>>>> scientifically testable by the way (i.e. to a lower standard of 'proof' >>>>>> than what we're used to around here). It's possible to write a program >>>>>> to >>>>>> shuffle an mm file, the prediction being that makes verification a lot >>>>>> less >>>>>> efficient. After that it might be possible to run some sort of >>>>>> regression >>>>>> on the timings. >>>>>> >>>>>> (I'm glossing over a lot of detail here, but a shuffle algorithm 1. >>>>>> makes a pass of an mm file to construct a DAG, 2. writes out a random >>>>>> axiom, 3. removes the axiom from the DAG which promotes any theorem no >>>>>> longer dependent on any axioms to the status of axiom (though obviously >>>>>> still outputted as a theorem), 4. return to step 2 until the whole file >>>>>> is >>>>>> written out) >>>>>> >>>>>> Best regards, >>>>>> >>>>>> Antony >>>>>> >>>>>> >>>>>> On Wed, May 11, 2022 at 5:21 PM Mario Carneiro <[email protected]> >>>>>> wrote: >>>>>> >>>>>>> It's true that O(n) is an approximation of the reality. If you >>>>>>> assume that array lookups can be done in O(1) (and there are at most >>>>>>> 2^word >>>>>>> size theorems total, which is almost certainly the case unless you have >>>>>>> a >>>>>>> "streaming" model for theorem verification, which is not the case for >>>>>>> most >>>>>>> proof systems), then you can get O(n) total time on a word RAM >>>>>>> computational model. There is another asterisk though which is that >>>>>>> theorems have to be O(1) in size for this to work. In general if >>>>>>> theorems >>>>>>> have size O(m) then verifying one metamath step takes O(m) so total >>>>>>> verification time is O(mn), so in the worst case, if you have a single >>>>>>> theorem whose statement takes up half of the entire file, you can spend >>>>>>> the >>>>>>> other half of the file applying that theorem O(n) times for O(n^2) >>>>>>> work. >>>>>>> This is the actual bound I have established for MM0 verification, but >>>>>>> if >>>>>>> you make a less pessimistic assumption it looks approximately linear. >>>>>>> (There are also complications getting this linear time bound in >>>>>>> metamath >>>>>>> when *expressions* stop being O(1): you can actually get exponential >>>>>>> size >>>>>>> terms in O(n) steps by reusing subproofs. MM0 uses dag-like sharing of >>>>>>> terms to circumvent this problem, but metamath fundamentally uses token >>>>>>> strings for its expressions so you have to get fancy with data >>>>>>> structures >>>>>>> in order to express such a highly redundant string without losing the >>>>>>> ability to freely reassociate token strings.) >>>>>>> >>>>>>> Setting aside the issues with large expressions and theorems and >>>>>>> returning to the lookup question, the reality is still more >>>>>>> complicated. If >>>>>>> you don't use a word RAM model and instead use functional data >>>>>>> structures, >>>>>>> then your array is actually a tree and then you get that O(n log n) >>>>>>> bound. >>>>>>> If you remember The Myth of RAM ( >>>>>>> http://www.ilikebigbits.com/2014_04_21_myth_of_ram_1.html) then you >>>>>>> will actually want to revise this to O(n sqrt n). But actually, it's a >>>>>>> bit >>>>>>> better than this because like regular programs, mathematics also has a >>>>>>> lot >>>>>>> of temporal and spatial locality, and this reflects in the fact that >>>>>>> the >>>>>>> theorems you access in the proof of a given theorem will often be hit >>>>>>> many >>>>>>> times and nearby theorems will also likely be accessed. So the usual >>>>>>> caching tricks work and it goes down to O(n sqrt s) where s is the >>>>>>> working >>>>>>> set size, which is difficult to quantify but general considerations of >>>>>>> how >>>>>>> humans work suggest that this should be roughly constant - each area of >>>>>>> mathematics generally has direct connections to O(1) other areas of >>>>>>> mathematics. So we're back to O(n) again. >>>>>>> >>>>>>> Mario >>>>>>> >>>>>>> On Wed, May 11, 2022 at 7:37 AM Antony Bartlett <[email protected]> >>>>>>> wrote: >>>>>>> >>>>>>>> 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 >>>>>>>> >>>>>>>> <https://groups.google.com/d/msgid/metamath/CAJ48g%2BCwN2q7qKqi5oh4WezRV75V%2BikgT9DJyT4_tbmO825yyQ%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/CAFXXJSuz8Q5Hxcu7U3iV6%3DU2KwwbWg6dhiJEVj5ZJSTHpayA_A%40mail.gmail.com >>>>>>> >>>>>>> <https://groups.google.com/d/msgid/metamath/CAFXXJSuz8Q5Hxcu7U3iV6%3DU2KwwbWg6dhiJEVj5ZJSTHpayA_A%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%2BDNwi2KhpTfYh%2BgfSTYd%2BV33Qmr_hWNfLSn3O6OnfgBXQ%40mail.gmail.com >>>>>> >>>>>> <https://groups.google.com/d/msgid/metamath/CAJ48g%2BDNwi2KhpTfYh%2BgfSTYd%2BV33Qmr_hWNfLSn3O6OnfgBXQ%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/CAFXXJSvYQQn1sDmjt1E_czs_vAuROUTTDVnWZpjC%3DjkaVSTWVA%40mail.gmail.com >>>>> >>>>> <https://groups.google.com/d/msgid/metamath/CAFXXJSvYQQn1sDmjt1E_czs_vAuROUTTDVnWZpjC%3DjkaVSTWVA%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/c1a69dcd-249e-40fc-b85c-ed62d5b4de0bn%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/c1a69dcd-249e-40fc-b85c-ed62d5b4de0bn%40googlegroups.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/16c8a2a7-f965-4414-9365-8657cca775c3n%40googlegroups.com.
