|
|
|
|
|
|
by cubefox
739 days ago
|
|
|
The thing is, when AI systems are able to translate intuitive natural language proofs into formal Lean code, they will also be used to translate intuitive concepts into formal Lean definitions. And then we can't be sure whether those definitions actually define the concepts they are named after. |
|
|