Metamath2Py: Python Translation of Metamath Theorems & Dataset Release
96 views
Skip to first unread message
Pavel Kamenev
Apr 22, 2025, 2:46:57 PMApr 22
to Metamath
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.
github repository: https://github.com/kamushekp/metamath2py/tree/main
github repository: https://github.com/kamushekp/metamath2py/tree/main
in particular,
hugginface dataset: https://huggingface.co/datasets/kamushekp/Metamath2Py
I welcome any questions, feedback, or critique on the dataset, code, or paper.
P.S. I’m also considering submitting this paper to arXiv, but as a first‑time submitter I need an endorsement. If anyone here can endorse me, I’d be grateful. https://arxiv.org/auth/endorse?x=NA8HI3 (Endorsement Code: NA8HI3)
Best regards, Pavel
David A. Wheeler
Apr 23, 2025, 11:18:47 AMApr 23
to Metamath Mailing List
> On Apr 22, 2025, at 1:07 PM, Pavel Kamenev <kamu...@gmail.com> 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.
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 )
Pavel Kamenev
Apr 29, 2025, 3:19:38 PMApr 29
to Metamath
Thank you for the detailed reply!
I definitely agree that uncompressed proofs are crucial. However, I still think syntax will remain a challenge for most LLMs, simply because Metamath is a low-resource language — it's underrepresented in training data compared to, for example, Python. So even if we provide clean proof traces, models might still fail to interpret them correctly unless they’ve seen enough Metamath-like structure during pretraining.
However, I’ve been watching the reasoning abilities of state-of-the-art LLMs like ChatGPT, and I think we’re getting close to the point where models can “absorb” the Metamath rules on the fly, even without prior exposure - just by pattern recognition, structural reasoning, etc - how human behave. So maybe this will become less of an issue soon thanks to the models' growing "intelligence".
I like the idea of training backward from the goal - I’ll try experimenting with that.
Thanks again for your thoughts, very helpful!
среда, 23 апреля 2025 г. в 22:18:47 UTC+7, David A. Wheeler:
Reply all
Reply to author
Forward
0 new messages