I think it’s all great. I have been interested in picking up something like Coq before. I only made my comment to reflect my personal tempered expectations. Ma

I think it’s all great. I have been interested in picking up something like Coq before. I only made my comment to reflect my personal tempered expectations. Maybe I am completely wrong, but just don’t see how it could wholly replace how mathematics is done and generated, but I do see how it could helpfully augment. I think the analogy is in the fancy type system programming languages like Haskell and Idris and the like, which are not practically affecting how people generally write programs and build systems. In both mathematics and writing programs, one must come up with something that models the solution needed for a given problem or system even if one can formally verify it afterwards, but that first part is the hard part (especially in programming since the assumptions in mathematics are quite explicit and known). I suppose there could be or are systems that generate techniques and proofs rather than merely verify, but I can only imagine that being an intractable problem and one not likely to be practically solved soon.