> On Feb 16, 2023, at 6:36 PM, Jon P <[email protected]> wrote:
>
> Mmm yeah interesting, I agree $2600 and then more for inference is quite a
> lot. I think your original plan might be quite a good one as if multiple
> groups are going to scrape the web for training data then we might be able to
> get into a bunch of different models.
>
> This is an interesting conversation with chatGPT. Seems it already knows
> quite a lot.
That is *utterly* fascinating. Especially since we certainly didn't present
data in a format that's easy to train on.
Many of its general-purpose text answers are right, too.
> ChatGPT:
> 6 1,5 eqtrans $p |- TarskiG = TarskiGC $
> 7 subst $e |- ( ( ph -> G e. TarskiGC ) -> ( ph -> G e. TarskiG ) ) $
> 8 hyp $e, ph |- ph $
> 9, 10 mp $e |- ( ph -> G e. TarskiG ) $
> 11 7, 9 mp $e |- ( ph -> G e. TarskiGC ) $
> 12 eqtrans $p |- ( ph -> G e. TarskiGC ) = ( ph -> G e. ( ( TarskiGC i^i
> TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base f ) / p ]. [. ( Itv f ) / i ].
> ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y )
> / x e. ( z i y ) / y e. ( x i z ) ) } ) } ) ) ) $
> 13 6, 11, 12 impbii $p |- ( ph -> ( X .- Y ) = ( Y .- X ) ) $
I compared that to the actual continuation of axtgcgrrflx (below). ChatGPT does
manage to look similar in terms for format. It doesn't manage to figure out
much in the way of the actual steps (either statement to use nor resulting
statement), which is too bad, because that makes not useful even as a proof
hinting assistant.
That said, it's not particularly trained on it, and the public-available data
certainly doesn't make it easy to train on. It's possible a tool specifically
trained on the dataset would do much better.
> Me:
> how many theorems are proven in the metamath database
>
> ChatGPT:
> As of the latest update to the Metamath database on January 24, 2022, there
> are a total of 272,443 theorems that have been proven. However, it's worth
> noting that this number may change as new theorems are added to the database
> over time.
Looking at just set.mm, it has 203588 statements; 2716 are $a and 40627 are $p.
Once you add the other databases (especially iset.mm), maybe there are around
270,000 statements
across all metamath databases. So perhaps it's confusing "theorem" with
"statement".
--- David A. Wheeler
========
Here's the actual current proof (ChatGPT was given 1-5):
1 df-trkg $a |- TarskiG = ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB
i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p
, y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e.
( x i z ) ) } ) } ) )
2 inss1 $p |- ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [.
( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \
{ x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) }
) } ) ) C_ ( TarskiGC i^i TarskiGB )
3 inss1 $p |- ( TarskiGC i^i TarskiGB ) C_ TarskiGC
4 2,3 sstri $p |- ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [.
( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \
{ x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) }
) } ) ) C_ TarskiGC
5 1,4 eqsstri $p |- TarskiG C_ TarskiGC
6 axtrkg.g $e |- ( ph -> G e. TarskiG )
7 5,6 sseldi $p |- ( ph -> G e. TarskiGC )
8 axtrkg.p $e |- P = ( Base ` G )
9 axtrkg.d $e |- .- = ( dist ` G )
10 axtrkg.i $e |- I = ( Itv ` G )
11 8,9,10 istrkgc $p |- ( G e. TarskiGC <-> ( G e. _V /\ ( A. x e. P A. y e. P
( x .- y ) = ( y .- x ) /\ A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .-
z ) -> x = y ) ) ) )
12 11 simprbi $p |- ( G e. TarskiGC -> ( A. x e. P A. y e. P ( x .- y ) = (
y .- x ) /\ A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y )
) )
13 12 simpld $p |- ( G e. TarskiGC -> A. x e. P A. y e. P ( x .- y ) = ( y
.- x ) )
14 7,13 syl $p |- ( ph -> A. x e. P A. y e. P ( x .- y ) = ( y .- x ) )
15 axtgcgrrflx.1 $e |- ( ph -> X e. P )
16 axtgcgrrflx.2 $e |- ( ph -> Y e. P )
17 oveq1 $p |- ( x = X -> ( x .- y ) = ( X .- y ) )
18 oveq2 $p |- ( x = X -> ( y .- x ) = ( y .- X ) )
19 17,18 eqeq12d $p |- ( x = X -> ( ( x .- y ) = ( y .- x ) <-> ( X .- y ) = (
y .- X ) ) )
20 oveq2 $p |- ( y = Y -> ( X .- y ) = ( X .- Y ) )
21 oveq1 $p |- ( y = Y -> ( y .- X ) = ( Y .- X ) )
22 20,21 eqeq12d $p |- ( y = Y -> ( ( X .- y ) = ( y .- X ) <-> ( X .- Y ) = (
Y .- X ) ) )
23 19,22 rspc2v $p |- ( ( X e. P /\ Y e. P ) -> ( A. x e. P A. y e. P ( x .- y
) = ( y .- x ) -> ( X .- Y ) = ( Y .- X ) ) )
24 15,16,23 syl2anc $p |- ( ph -> ( A. x e. P A. y e. P ( x .- y ) = ( y .- x
) -> ( X .- Y ) = ( Y .- X ) ) )
--
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/26351560-5A3C-480B-9525-C3A5ADE7BD46%40dwheeler.com.
