I started a GitHub repository for an AI Generative Pretrained Transformer model for Metamath. It is base on a youtube video by Andrej Karpathy (Building makemore Part 2: MLP).
An example prompt and reply by the model is: You: <|start_claim|> <|given|> |- G : _om -1-1-onto-> Z <|given|> |- ( G : _om -1-1-onto-> Z -> `' G : Z -1-1-onto-> _om ) <|given|> |- ( `' G : Z -1-1-onto-> _om -> `' G : Z --> _om ) <|conclude|> Model: |- `' G : Z --> _om <|end_claim|> It is just a start: there is no interface to 'chat'. It is more of a proof of concept. -- 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/132a41df-6275-4941-b394-a732b6354503n%40googlegroups.com.
