Topic: a poem about formalization
Jeremy Avigad (Jul 29 2022 at 23:39):
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,
and more powerful.
As we formalize mathematics,
we open new doors to discovery,
and create new ways to see the world.
Heather Macbeth (Jul 29 2022 at 23:52):
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 (Jul 29 2022 at 23:59):
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 (Jul 30 2022 at 00:23):
Kyle Miller (Jul 30 2022 at 00:25):
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.
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 (Jul 30 2022 at 00:27):
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 (Jul 30 2022 at 00:28):
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 (Jul 30 2022 at 00:31):
@Jason Rute Thanks for the tip, I'm trying this now and getting better results!
Last updated: Aug 03 2023 at 10:10 UTC