a poem about formalization

Stream: general

[Jeremy Avigad]

I just tried the openAI playground (https://openai.com/api/) for the first time. In response to the prompt "write a poem about formalization and the future of mathematics," it wrote the poem that follows. I have to say, I kind of like it.

As we formalize mathematics,
we create a language
for describing the world.

We build upon the work of past generations,
Adding new symbols and concepts
to describe the patterns we see.

With each new generation,
math becomes more precise,
more complete,
and more powerful.

As we formalize mathematics,
we open new doors to discovery,
and create new ways to see the world.

[Heather Macbeth]

I was really impressed with this poem, but my own experiment, with the prompt "Prove that the sum of two odd numbers is even," was ... less impressive.

The sum of two odd numbers is even because the sum of two numbers is the result of adding the two numbers together. If one number is even and one number is odd, the sum of the two numbers is still even.

[Anatole Dedecker]

Ok I found something funny, by writing `add_succ_zero :ˋ I got what looks like a portion of a Coq file with proofs of properties of addition

[Jason Rute]

(deleted)

[Kyle Miller]

Last quarter I generated a review sheet for my combinatorics course with openAI, and as part of our midterm review session we went through it to figure out how it was wrong and how to fix it.

Some favorites:

Example. A group of 10 people are sitting around a table. Show that there must be two people sitting next to each other who have the same birthday.

Solution. There are 10 people and 365 days in a year, so by the pigeonhole principle, two people must have the same birthday.

Example. There are 12 eggs in a carton. Show that there must be two eggs with the same weight.

Solution. There are 12 eggs and there are only so many different weights that eggs can have, so by the pigeonhole principle, two eggs must have the same weight.

[Jason Rute]

@Heather Macbeth
This prompt probably works better and is a bit more consistent for me.

Theorem: The sum of two odd numbers is even.
Proof.

If you prompt with

Prove that the sum of two odd numbers is even.

it might just repeat the question with different versions, like it is given a homework problem sheet. Here is the response from Codex, which has a bit more math in it's training than GPT-3, but GPT-3 also gave me the same basic proof.

Theorem: The sum of two odd numbers is even.
Proof. Let $a$ and $b$ be odd numbers. Then $a = 2k + 1$ and $b = 2l + 1$ for some integers $k$ and $l$. Then $a + b = 2k + 1 + 2l + 1 = 2(k + l) + 2 = 2(k + l + 1)$, which is even.

[Jason Rute]

Also, while it is not as fun, the best way to make these model do what you want is to give a few examples in the prompt.

[Heather Macbeth]

@Jason Rute Thanks for the tip, I'm trying this now and getting better results!