Blue AGI

Stream: general

[Jon Eugster]

(Starting a discussion stream for the announcement here.)

First of all, nice work @Michael Bucko .

I think the proofs the model creates are miss-formated, as your own screenshot already shows, but here is another:
Screenshot_20240215_105720.png

Generally, with mathlib's and lean's active development I find it hard to get anything useful out of any AI model that uses old training data (it claims itself to be trained on 2021 data when asked). i.e. it produces lean3 code and does not know that mathlib4 even exists. Moreover, it did not understand follow-up questions and just interpreted them as new questions without context (as far as I can tell) which made it hard to specify/correct things.

I don't know how they work behind the scene, but moogle and loogle are two great lean-related AI tools, which are useful to explore the most recent version of mathlib, and maybe there are synergies there that could be used.

[Yaël Dillies]

(wrong person!)

[Jon Eugster]

yep :face_palm:

[Jireh Loreaux]

Loogle isn't AI.

[Yaël Dillies]

Well, it is, right? Good old-fashioned AI, AI nonetheless.

[Michael Bucko]

Thank you, Jon. I so much appreciate your feedback!

We'll definitely work on formatting. It's gonna get better.

As for mathlib3 vs mathlib4, we're already trying to support mathlib4 as much as possible. Supporting Mathlib4 is very important to us.

You will also be able write Lean and Python code too, with all the CI/CD workflows and git-related tooling around it. And it's not only going to be a chat. Our goal is to automate proof writing and introduce a new way of collaborative proof writing.

[Michael Bucko]

(Our inspiration comes from the PFR formalization project, Kontorovich-Tao formalising PNT, and the Liquid Tensor project. We've been creating "blueprints" and creating snippets of Lean4. Now, we're trying to make all of this available through this web solution)

[Eric Rodriguez]

Yaël Dillies said:

Well, it is, right? Good old-fashioned AI, AI nonetheless.

it's literally just a search program - it doesn't try and rank anything at all.

[Ruben Van de Velde]

Searching is pretty intelligent

[Eric Rodriguez]

It's a type-correct regex; I don't really want to bikeshed about what AI is but I feel like Loogle is very far from it. Moogle's integration with it, however

[Michael Bucko]

Our goal is to do some sort of CI/CD for Lean + Python, and train the relevant models (as well as use the foundational models). I wrote down some thoughts:

• inspiration from the Liquid Tensor project: https://buildermath.substack.com/p/liquid-tensor-language-and-formalization
• collaborative proofs in the math-as-code and code-as-math setting: https://buildermath.substack.com/p/collaborative-proof-development-is
• UX behind math (please share your feedback as always): https://buildermath.substack.com/p/lines-and-universes
• AlphaGeometry insights: https://buildermath.substack.com/p/transformer-xl-with-sliding-window
• Gan–Gross–Prasad-inspired insights for our engineering efforts: https://buildermath.substack.com/p/orbit-method-automorphic-forms-and

Please share your thoughts & feedback!

[Jon Eugster]

you're of course right @Jireh Loreaux, as always. Just shows I've never actually looked at what it does ;)

[Jireh Loreaux]

I'm certainly not always right! :rofl:

[Brendan Seamas Murphy]

Why does this brand itself as "AGI"?

[Michael Bucko]

Ah, that's just for the future. Building towards something that could generate parts of proofs together with professional mathematicians.

[Michael Bucko]

We're far away from AGI atm. I think it'll be just BLUE.