Timeline for Make ChatGPT write formal proof from natural language proof
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 8, 2023 at 1:15 | comment | added | Bruce Adams | @AndrejBauer there is ai.stackexchange.com which covers AI in general and not just chatGPT | |
| Mar 17, 2023 at 4:59 | vote | accept | domotorp | ||
| Mar 17, 2023 at 0:32 | answer | added | Jason Rute | timeline score: 7 | |
| Mar 16, 2023 at 22:32 | answer | added | Joey Eremondi | timeline score: 6 | |
| Mar 16, 2023 at 21:59 | comment | added | Andrej Bauer | Someone please create a StackExchange site about ChatGPT. | |
| Mar 16, 2023 at 21:57 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
deleted 8 characters in body
|
| Mar 16, 2023 at 20:54 | comment | added | domotorp | @Will ChatGPT is not bad at writing codes in programming languages, so that's why I think this might have a chance. Maybe next year then. | |
| Mar 16, 2023 at 19:43 | comment | added | Will Sawin | I don't think the training data for Chat-GPT is public but it surely a vanishingly small percent of it is Lean code, and whatever is there is most likely a mix of different versions, so there is no one correct version to use. Theoretically a similar model fine-tuned on a current version of mathlib should perform much better. | |
| Mar 16, 2023 at 17:46 | comment | added | Eric |
"not good enough in lean" is subjective unless you mean "outputs valid lean code". With that meaning, ChatGPT clearly isn't good enough, as it forgot the preamble! import algebra.big_operators.basic, import tactic.ring is the missing preamble, although the code still doesn't work.
|
|
| Mar 16, 2023 at 17:42 | history | edited | Eric | CC BY-SA 4.0 |
Syntax highlight
|
| S Mar 16, 2023 at 17:36 | review | First questions | |||
| Mar 17, 2023 at 0:36 | |||||
| S Mar 16, 2023 at 17:36 | history | asked | domotorp | CC BY-SA 4.0 |