> On Apr 22, 2025, at 1:07 PM, Pavel Kamenev <[email protected]> wrote: > > About a year and a half ago I dove into the Metamath system with the goal > of creation of LLM-based automatical theorem proover. I had trouble with the > fact that Metamath seemed to be under-represented in the training sets of > Chat-GPT and others, and so its syntax and proof semantics were hard for the > models to understand. I solved this by rewriting mmverify.py to map > Metamath’s floating and essential hypotheses, assertions, and proof steps to > executable Python classes. It seemed reasonable to me to share these > intermediate results and publish a short article, dataset and source code. That's an interesting approach, thanks for sharing it! I've also been thinking about this, though from a different angle: 1. LLMs struggle with compressed proofs; it's important to provide *uncompressed* proofs in training sets. 2. In theory the LLM could simply output the proof steps, but I think they need the intermediate results so they have more information to "work with" to verify that they're going the right way. 3. LLMs struggle to produce specific "final results". I speculate that training going *backwards*, starting from the final goal, will produce a better-working result. 4. Instead of Python-looking, I think it'd be more effective to use something like metamath set.mm; set scroll continuous; show proof fsumdvdsmul /reverse and omit the step numbers. What I have in mind is below. --- David A. Wheeler === EXAMPLE === 801 fsumdvdsmul=3eqtrd $p |- ( ph -> ( sum_ j e. X A x. sum_ k e. Y B ) = sum_ i e. Z C ) 800 3eqtrd.3=3eqtr4a $p |- ( ph -> sum_ j e. X sum_ k e. Y D = sum_ i e. Z C ) 799 3eqtr4a.3=eqtrid $p |- ( ph -> sum_ i e. Z C = sum_ z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C ) 798 eqtrid.2=fsumf1o $p |- ( ph -> sum_ w e. Z [_ w / i ]_ C = sum_ z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C ) 797 fsumf1o.5=r19.21bi $p |- ( ( ph /\ w e. Z ) -> [_ w / i ]_ C e. CC ) 796 r19.21bi.1=mpbid $p |- ( ph -> A. w e. Z [_ w / i ]_ C e. CC ) 795 mpbid.maj=bitr3id $p |- ( ph -> ( A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC <-> A. w e. Z [_ w / i ]_ C e. CC ) ) 794 bitr3id.2=raleqdv $p |- ( ph -> ( A. w e. ( ( x e. CC , y e. CC |-> ( x x. y ) ) " ( X X. Y ) ) [_ w / i ]_ C e. CC <-> A. w e. Z [_ w / i ]_ C e. CC ) ) 793 raleqdv.1=eqtrid $p |- ( ph -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) " ( X X. Y ) ) = Z ) 792 eqtrid.2=3syl $p |- ( ph -> ran ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) = Z ) 791 3syl.3=forn $p |- ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -onto-> Z -> ran ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) = Z ) 787 3syl.2=f1ofo $p |- ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -onto-> Z ) 783 3syl.1=528 $p |- ( ph -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z ) 770 eqtrid.1=df-ima $a |- ( ( x e. CC , y e. CC |-> ( x x. y ) ) " ( X X. Y ) ) = ran ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) 757 bitr3id.1=mp2an $p |- ( A. w e. ( ( x e. CC , y e. CC |-> ( x x. y ) ) " ( X X. Y ) ) [_ w / i ]_ C e. CC <-> A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) 756 mp2an.3=ralima $p |- ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) Fn ( CC X. CC ) /\ ( X X. Y ) C_ ( CC X. CC ) ) -> ( A. w e. ( ( x e. CC , y e. CC |-> ( x x. y ) ) " ( X X. Y ) ) [_ w / i ]_ C e. CC <-> A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) ) 755 rexima.x=eleq1d $p |- ( w = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) -> ( [_ w / i ]_ C e. CC <-> [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) ) 754 eleq1d.1=499 $p |- ( w = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) -> [_ w / i ]_ C = [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C ) 740 mp2an.2=mp2an $p |- ( X X. Y ) C_ ( CC X. CC ) 739 mp2an.3=xpss12 $p |- ( ( X C_ CC /\ Y C_ CC ) -> ( X X. Y ) C_ ( CC X. CC ) ) 734 mp2an.2=332 $p |- Y C_ CC 733 mp2an.1=317 $p |- X C_ CC 725 mp2an.1=ax-mp $a |- ( x e. CC , y e. CC |-> ( x x. y ) ) Fn ( CC X. CC ) 724 maj=ffn $p |- ( ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC -> ( x e. CC , y e. CC |-> ( x x. y ) ) Fn ( CC X. CC ) ) 720 min=mpomulf $p |- ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC 692 mpbid.min=syl $p |- ( ph -> A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) 691 syl.2=sylbi $p |- ( A. z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C e. CC -> A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) 690 sylbi.2=ralrimiv $p |- ( A. w e. ( X X. Y ) [_ ( x. ` w ) / i ]_ C e. CC -> A. z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) 689 ralrimiv.1=com12 $p |- ( A. w e. ( X X. Y ) [_ ( x. ` w ) / i ]_ C e. CC -> ( z e. ( X X. Y ) -> [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) ) 688 com12.1=rspcdv $p |- ( z e. ( X X. Y ) -> ( A. w e. ( X X. Y ) [_ ( x. ` w ) / i ]_ C e. CC -> [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) ) 687 rspcdv.2=bitr3d $p |- ( ( z e. ( X X. Y ) /\ w = z ) -> ( [_ ( x. ` w ) / i ]_ C e. CC <-> [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) ) 686 bitr3d.2=adantr $p |- ( ( z e. ( X X. Y ) /\ w = z ) -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) ) 685 adantr.1=eleq1d $p |- ( z e. ( X X. Y ) -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C e. CC ) ) 684 eleq1d.1=369 $p |- ( z e. ( X X. Y ) -> [_ ( x. ` z ) / i ]_ C = [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C ) 674 bitr3d.1=eleq1d $p |- ( ( z e. ( X X. Y ) /\ w = z ) -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> [_ ( x. ` w ) / i ]_ C e. CC ) ) 673 eleq1d.1=adantl $p |- ( ( z e. ( X X. Y ) /\ w = z ) -> [_ ( x. ` z ) / i ]_ C = [_ ( x. ` w ) / i ]_ C ) 672 adantl.1=eqcoms $p |- ( w = z -> [_ ( x. ` z ) / i ]_ C = [_ ( x. ` w ) / i ]_ C ) 671 eqcoms.1=633 $p |- ( z = w -> [_ ( x. ` z ) / i ]_ C = [_ ( x. ` w ) / i ]_ C ) 650 rspcdv.1=id $p |- ( z e. ( X X. Y ) -> z e. ( X X. Y ) ) 635 sylbi.1=cbvralvw $p |- ( A. z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C e. CC <-> A. w e. ( X X. Y ) [_ ( x. ` w ) / i ]_ C e. CC ) 634 cbvralvw.1=eleq1d $p |- ( z = w -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> [_ ( x. ` w ) / i ]_ C e. CC ) ) 633 633:eleq1d.1=csbeq1d $p |- ( z = w -> [_ ( x. ` z ) / i ]_ C = [_ ( x. ` w ) / i ]_ C ) 632 csbeq1d.1=fveq2 $p |- ( z = w -> ( x. ` z ) = ( x. ` w ) ) 599 syl.1=sylibr $p |- ( ph -> A. z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C e. CC ) 598 sylibr.2=ralxp $p |- ( A. z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C e. CC <-> A. j e. X A. k e. Y D e. CC ) 597 ralxp.1=eleq1d $p |- ( z = <. j , k >. -> ( [_ ( x. ` z ) / i ]_ C e. CC <-> D e. CC ) ) 596 eleq1d.1=424 $p |- ( z = <. j , k >. -> [_ ( x. ` z ) / i ]_ C = D ) 584 sylibr.1=ralrimivva $p |- ( ph -> A. j e. X A. k e. Y D e. CC ) 583 ralrimivva.1=454 $p |- ( ( ph /\ ( j e. X /\ k e. Y ) ) -> D e. CC ) 540 fsumf1o.4=adantl $p |- ( ( ph /\ z e. ( X X. Y ) ) -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` z ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) ) 539 adantl.1=fvres $p |- ( z e. ( X X. Y ) -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` z ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) ) 528 528:fsumf1o.3=mpodvdsmulf1o $p |- ( ph -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z ) 527 mpodvdsmulf1o.z=mpodvdsmulf1o.z $e |- Z = { x e. NN | x || ( M x. N ) } 526 mpodvdsmulf1o.y=mpodvdsmulf1o.y $e |- Y = { x e. NN | x || N } 525 mpodvdsmulf1o.x=mpodvdsmulf1o.x $e |- X = { x e. NN | x || M } 524 mpodvdsmulf1o.3=mpodvdsmulf1o.3 $e |- ( ph -> ( M gcd N ) = 1 ) 523 mpodvdsmulf1o.2=mpodvdsmulf1o.2 $e |- ( ph -> N e. NN ) 522 mpodvdsmulf1o.1=mpodvdsmulf1o.1 $e |- ( ph -> M e. NN ) 513 fsumf1o.2=syl2anc $p |- ( ph -> ( X X. Y ) e. Fin ) 512 syl2anc.3=xpfi $p |- ( ( X e. Fin /\ Y e. Fin ) -> ( X X. Y ) e. Fin ) 509 syl2anc.2=109 $p |- ( ph -> Y e. Fin ) 508 syl2anc.1=70 $p |- ( ph -> X e. Fin ) 499 499:fsumf1o.1=csbeq1 $p |- ( w = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) -> [_ w / i ]_ C = [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C ) 483 eqtrid.1=cbvsumi $p |- sum_ i e. Z C = sum_ w e. Z [_ w / i ]_ C 482 cbvsumi.3=csbeq1a $p |- ( i = w -> C = [_ w / i ]_ C ) 478 cbvsumi.2=nfcsb1v $p |- F/_ i [_ w / i ]_ C 474 cbvsumi.1=nfcv $p |- F/_ w C 455 3eqtr4a.2=fsumxp $p |- ( ph -> sum_ j e. X sum_ k e. Y D = sum_ z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C ) 454 454:fsumxp.4=eqeltrrd $p |- ( ( ph /\ ( j e. X /\ k e. Y ) ) -> D e. CC ) 453 eqeltrrd.2=mulcld $p |- ( ( ph /\ ( j e. X /\ k e. Y ) ) -> ( A x. B ) e. CC ) 452 addcld.2=adantrl $p |- ( ( ph /\ ( j e. X /\ k e. Y ) ) -> B e. CC ) 451 adant2.1=fsumdvdsmul.5 $e |- ( ( ph /\ k e. Y ) -> B e. CC ) 446 addcld.1=adantrr $p |- ( ( ph /\ ( j e. X /\ k e. Y ) ) -> A e. CC ) 445 adant2.1=fsumdvdsmul.4 $e |- ( ( ph /\ j e. X ) -> A e. CC ) 435 eqeltrrd.1=fsumdvdsmul.6 $e |- ( ( ph /\ ( j e. X /\ k e. Y ) ) -> ( A x. B ) = D ) 426 fsumxp.3=109 $p |- ( ph -> Y e. Fin ) 425 fsumxp.2=70 $p |- ( ph -> X e. Fin ) 424 424:fsumxp.1=eqtrdi $p |- ( z = <. j , k >. -> [_ ( x. ` z ) / i ]_ C = D ) 423 eqtrdi.2=csbie $p |- [_ ( j x. k ) / i ]_ C = D 422 csbie.2=fsumdvdsmul.7 $e |- ( i = ( j x. k ) -> C = D ) 421 csbie.1=ovex $p |- ( j x. k ) e. _V 413 eqtrdi.1=csbeq1d $p |- ( z = <. j , k >. -> [_ ( x. ` z ) / i ]_ C = [_ ( j x. k ) / i ]_ C ) 412 csbeq1d.1=eqtr4di $p |- ( z = <. j , k >. -> ( x. ` z ) = ( j x. k ) ) 411 eqtr4di.2=df-ov $a |- ( j x. k ) = ( x. ` <. j , k >. ) 407 eqtr4di.1=fveq2 $p |- ( z = <. j , k >. -> ( x. ` z ) = ( x. ` <. j , k >. ) ) 370 3eqtr4a.1=sumeq2i $p |- sum_ z e. ( X X. Y ) [_ ( x. ` z ) / i ]_ C = sum_ z e. ( X X. Y ) [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C 369 369:sumeq2i.1=csbeq1d $p |- ( z e. ( X X. Y ) -> [_ ( x. ` z ) / i ]_ C = [_ ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) / i ]_ C ) 368 csbeq1d.1=eqcomd $p |- ( z e. ( X X. Y ) -> ( x. ` z ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) ) 367 eqcomd.1=syl $p |- ( z e. ( X X. Y ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) = ( x. ` z ) ) 366 syl.2=exlimivv $p |- ( E. u E. v ( z = <. u , v >. /\ ( u e. X /\ v e. Y ) ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) = ( x. ` z ) ) 365 exlimivv.1=impel $p |- ( ( z = <. u , v >. /\ ( u e. X /\ v e. Y ) ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) = ( x. ` z ) ) 364 impel.2=syl2an $p |- ( ( u e. X /\ v e. Y ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( x. ` <. u , v >. ) ) 363 syl2an.3=3eqtr3g $p |- ( ( u e. CC /\ v e. CC ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( x. ` <. u , v >. ) ) 362 3eqtr3g.3=df-ov $a |- ( u x. v ) = ( x. ` <. u , v >. ) 358 3eqtr3g.2=df-ov $a |- ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) 354 3eqtr3g.1=ovmpot $p |- ( ( u e. CC /\ v e. CC ) -> ( u ( x e. CC , y e. CC |-> ( x x. y ) ) v ) = ( u x. v ) ) 333 syl2an.2=sseli $p |- ( v e. Y -> v e. CC ) 332 332:sseli.1=sstri $p |- Y C_ CC 331 sstri.2=nnsscn $p |- NN C_ CC 330 sstri.1=ssrab3 $p |- Y C_ NN 329 ssrab3.1=mpodvdsmulf1o.y $e |- Y = { x e. NN | x || N } 318 syl2an.1=sseli $p |- ( u e. X -> u e. CC ) 317 317:sseli.1=sstri $p |- X C_ CC 316 sstri.2=nnsscn $p |- NN C_ CC 315 sstri.1=ssrab3 $p |- X C_ NN 314 ssrab3.1=mpodvdsmulf1o.x $e |- X = { x e. NN | x || M } 294 impel.1=biimpd $p |- ( z = <. u , v >. -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( x. ` <. u , v >. ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) = ( x. ` z ) ) ) 293 biimpd.1=eqeq12d $p |- ( z = <. u , v >. -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( x. ` <. u , v >. ) <-> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) = ( x. ` z ) ) ) 292 eqeq12d.2=eqcoms $p |- ( z = <. u , v >. -> ( x. ` <. u , v >. ) = ( x. ` z ) ) 291 eqcoms.1=fveq2 $p |- ( <. u , v >. = z -> ( x. ` <. u , v >. ) = ( x. ` z ) ) 282 eqeq12d.1=eqcoms $p |- ( z = <. u , v >. -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) ) 281 eqcoms.1=fveq2 $p |- ( <. u , v >. = z -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. u , v >. ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` z ) ) 250 syl.1=elxpi $p |- ( z e. ( X X. Y ) -> E. u E. v ( z = <. u , v >. /\ ( u e. X /\ v e. Y ) ) ) 174 3eqtrd.2=sumeq2dv $p |- ( ph -> sum_ j e. X ( A x. sum_ k e. Y B ) = sum_ j e. X sum_ k e. Y D ) 173 sumeq2dv.1=eqtrd $p |- ( ( ph /\ j e. X ) -> ( A x. sum_ k e. Y B ) = sum_ k e. Y D ) 172 eqtrd.2=sumeq2dv $p |- ( ( ph /\ j e. X ) -> sum_ k e. Y ( A x. B ) = sum_ k e. Y D ) 171 sumeq2dv.1=anassrs $p |- ( ( ( ph /\ j e. X ) /\ k e. Y ) -> ( A x. B ) = D ) 170 anassrs.1=fsumdvdsmul.6 $e |- ( ( ph /\ ( j e. X /\ k e. Y ) ) -> ( A x. B ) = D ) 158 eqtrd.1=fsummulc2 $p |- ( ( ph /\ j e. X ) -> ( A x. sum_ k e. Y B ) = sum_ k e. Y ( A x. B ) ) 157 fsummulc2.3=adantlr $p |- ( ( ( ph /\ j e. X ) /\ k e. Y ) -> B e. CC ) 156 adant2.1=fsumdvdsmul.5 $e |- ( ( ph /\ k e. Y ) -> B e. CC ) 146 fsummulc2.2=fsumdvdsmul.4 $e |- ( ( ph /\ j e. X ) -> A e. CC ) 145 fsummulc2.1=adantr $p |- ( ( ph /\ j e. X ) -> Y e. Fin ) 144 adantr.1=109 $p |- ( ph -> Y e. Fin ) 113 3eqtrd.1=fsummulc1 $p |- ( ph -> ( sum_ j e. X A x. sum_ k e. Y B ) = sum_ j e. X ( A x. sum_ k e. Y B ) ) 112 fsummulc2.3=fsumdvdsmul.4 $e |- ( ( ph /\ j e. X ) -> A e. CC ) 111 fsummulc2.2=fsumcl $p |- ( ph -> sum_ k e. Y B e. CC ) 110 fsumcl.2=fsumdvdsmul.5 $e |- ( ( ph /\ k e. Y ) -> B e. CC ) 109 109:fsumcl.1=ssfid $p |- ( ph -> Y e. Fin ) 108 ssfid.2=eqsstrid $p |- ( ph -> Y C_ ( 1 ... N ) ) 107 eqsstrid.2=syl $p |- ( ph -> { x e. NN | x || N } C_ ( 1 ... N ) ) 106 syl.2=dvdsssfz1 $p |- ( N e. NN -> { x e. NN | x || N } C_ ( 1 ... N ) ) 103 syl.1=mpodvdsmulf1o.2 $e |- ( ph -> N e. NN ) 95 eqsstrid.1=mpodvdsmulf1o.y $e |- Y = { x e. NN | x || N } 84 ssfid.1=fzfid $p |- ( ph -> ( 1 ... N ) e. Fin ) 70 70:fsummulc2.1=ssfid $p |- ( ph -> X e. Fin ) 69 ssfid.2=eqsstrid $p |- ( ph -> X C_ ( 1 ... M ) ) 68 eqsstrid.2=syl $p |- ( ph -> { x e. NN | x || M } C_ ( 1 ... M ) ) 67 syl.2=dvdsssfz1 $p |- ( M e. NN -> { x e. NN | x || M } C_ ( 1 ... M ) ) 64 syl.1=mpodvdsmulf1o.1 $e |- ( ph -> M e. NN ) 56 eqsstrid.1=mpodvdsmulf1o.x $e |- X = { x e. NN | x || M } 44 ssfid.1=fzfid $p |- ( ph -> ( 1 ... M ) e. Fin ) -- 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 visit https://groups.google.com/d/msgid/metamath/8E9E9513-8FD3-4DC1-AFCC-5118C48FC34C%40dwheeler.com.
Re: [Metamath] Metamath2Py: Python Translation of Metamath Theorems & Dataset Release
'David A. Wheeler' via Metamath Wed, 23 Apr 2025 08:18:54 -0700
- [Metamath] Metamath2Py: Python Translation... Pavel Kamenev
- Re: [Metamath] Metamath2Py: Python Tr... 'David A. Wheeler' via Metamath
- Re: [Metamath] Metamath2Py: Pytho... Pavel Kamenev
