Re:Mathematicians welcome computer-assisted proof in ‘grand ...
by zant on Sunday June 20, 2021 @03:42AM
(#27567993)
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.
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.