AI Generative Pretrained Transformer model for Metamath: GitHub

[bil...@gmail.com]

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.

[bil...@gmail.com]

I forgot the link: https://github.com/billh0420/ClaimGPT250203.git

[David A. Wheeler]

> On Feb 6, 2025, at 9:29 PM, bil...@gmail.com <bil...@gmail.com> wrote:
>
> 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).

Awesome! I've added a link to it from this page:

https://github.com/metamath/set.mm/wiki/Automated-proving

--- David A. Wheeler

[bil...@gmail.com]

I think I gave the wrong reference to the video by Andrej Karpathy that this project is based on. I think the correct reference is "Let's build GPT: from scratch, in code, spelled out."

If that is not correct, you might want to look at the link https://karpathy.ai/zero-to-hero.html (this webpage has links to a course by Andrej Karpathy on building neural networks, from scratch, in code.) The GitHub repository has the link https://github.com/karpathy/ng-video-lecture

Sorry that I don't remember which video from Andrej Karpathy that I based the project on.

"Deep Dive into LLMs like ChatGPT" is an amazing youtube video put out by Andrej Karpathy a few days ago (it is three and a half hours long). I think it has some concepts that might be useful for making AI work with Metamath.

Bill Hale

[David A. Wheeler]

> On Feb 7, 2025, at 3:57 PM, bil...@gmail.com <bil...@gmail.com> wrote:
>
> "Deep Dive into LLMs like ChatGPT" is an amazing youtube video put out by Andrej Karpathy

Great! I added those links to:

[Glauco]

Hi Bill,

Il giorno venerdì 7 febbraio 2025 alle 21:57:48 UTC+1 bil...@gmail.com wrote:

I think I gave the wrong reference to the video by Andrej Karpathy that this project is based on. I think the correct reference is "Let's build GPT: from scratch, in code, spelled out."

over the past few weeks, I’ve also been exploring Karpathy’s channel. Unfortunately, I ended up watching some of the videos out of order, and I keep hearing him reference past content. To address this, I’m now focusing on the "Make More" series and currently working through the first part (even though it doesn’t explicitly have "Part 1" in the title).

If you happen to recall the specific video and approximate timestamp where he discusses the model you’ve implemented, I’d greatly appreciate it. I’m really interested in learning more about it.

Thanks in advance!

Glauco

[Caleb Nwokocha]

C implementation of the machine learning program shown in the Jupyter notebook.

claim-gpt.c https://github.com/calebnwokocha/ClaimGPT250203/blob/main/claim-gpt.c
Jupter notebook https://github.com/billh0420/ClaimGPT250203/blob/main/claim_gpt.ipynb

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/b47c46ef-52c8-460c-ace0-fdd97330d038n%40googlegroups.com.

[bil...@gmail.com]

Glauco asked "If you happen to recall the specific video and approximate timestamp where he discusses the model you’ve implemented, I’d greatly appreciate it."

I can't seem to fine the specific video.

But the GitHub repo that I used is definitely:  https://github.com/karpathy/ng-video-lecture

I based my code on gpt.py (which I refactored into multiply py files). This file is 225 lines.

I ignored the file bigram.py.

This repo uses a Shakespeare corpus to generate Shakespeare like dialog.

I kept the model code in gpt.py and just replaced the Shakespeare corpus with a Metamath corpus that I generated from Python.