[runeks]

> 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.

[zant]

Yeah 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.

[fspeech]

Yes and the isomorphism is known as Curry-Howard Correspondence https://en.wikipedia.org/wiki/Curry-Howard_correspondence