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