I'm a professional mathematician and, candidly, most people in my subfield don't really know that they exist. I do, and would love to use them, but I find them very difficult to use and don't have good examples of proofs relevant to my work.
To be specific, I've used Coq in the past to help verify properties of programs such as a sorted list really being sorted. That said, I primarily work in applied math areas such as optimization, numerical linear algebra, and numerical PDEs and I have no idea where to begin with fundamental proofs such as Newton's method converging quadratically within a certain neighborhood of the solution. Alternatively, I'd love to see formalized proofs of the theorems that we'd learn in a course in real analysis such as one based on Rudin's Principles of Mathematical Analysis. Really, if anyone has examples of these, please let me know.
There's an amazing number of errors in published work. Most of the time, the work is still mostly right, but that's not OK. In my opinion, we'd be better off with formalized proofs.
To be specific, I've used Coq in the past to help verify properties of programs such as a sorted list really being sorted. That said, I primarily work in applied math areas such as optimization, numerical linear algebra, and numerical PDEs and I have no idea where to begin with fundamental proofs such as Newton's method converging quadratically within a certain neighborhood of the solution. Alternatively, I'd love to see formalized proofs of the theorems that we'd learn in a course in real analysis such as one based on Rudin's Principles of Mathematical Analysis. Really, if anyone has examples of these, please let me know.
There's an amazing number of errors in published work. Most of the time, the work is still mostly right, but that's not OK. In my opinion, we'd be better off with formalized proofs.