4 ms·
> But systems known as proof assistants go deeper. The user enters statements into the system to teach it the definition of a mathematical concept — an object —
by runeks 5y ago
> But systems known as proof assistants go deeper. The user enters statements into the system to teach it the definition of a mathematical concept — an object — based on simpler objects that the machine already knows about. A statement can also just refer to known objects, and the proof assistant will answer whether the fact is ‘obviously’ true or false based on its current knowledge.
As far as I can see this is just programming. How is this different from writing in Java
int i = “hello”
and seeing that the Java compiler rejects this “thesis”?
Of course, we need more complex types than “int” and “String”, but in principle it’s the same.
- fspeech 5y agoYes and the isomorphism is known as Curry-Howard Correspondence https://en.wikipedia.org/wiki/Curry-Howard_correspondence https://en.wikipedia.org/wiki/Curry-Howard_correspondence
- zant 5y agoYeah you can say that. You can also say that Machine Learning is just programming. Or in a similar way you can also say that First Order Logic is just programming. However, the cool thing about programming is that it lets us represent a lot of different things. In this case you're representing the construction and interaction of mathematical objects, with a language that targets a specific proof management system to verify this constructions. But yes, it is "just programming", and some functional languages even support proofs to some extent like Scala or Agda.