|
|
|
|
|
|
by vessenes
534 days ago
|
|
|
Interesting thoughts, thanks. It seems to me a model trained to generate Lean could also be purposed to explain a large Lean proof, and that’s very interesting. So much of modern math is limited to extremely small cohorts. None of that is dispositive inre provable safety, obviously. |
|
|