3 ms·

I really think that proof assistants like Coq are going to eventually be the future of math. Once they are less painful to use :( I spent a term working as a

by Tyr42 10y ago

I really think that proof assistants like Coq are going to eventually be the future of math. Once they are less painful to use :( I spent a term working as a research assistant on Coq, proving a new induction scheme for Featherweight Java classes. I came into the term quite hopeful, and already with some Coq experience, but I really don't feel like these tools are good enough to expect regular people to use. Even mathematicians. I'm hopeful that in the distant future, we can get some AI assistance going on, so that the proof assistant can actually assist, not just check and impede. I would like my month spent on transitivity of subclassing back :( It's really hard to use these tools as they are now.

bjz_ 10y ago
I've heard some from people that it's almost like we are still at 'the assembly language' level when it comes to theorem proving. We still have a great deal to build in order to be productive at higher levels of abstraction.
eli_gottlieb 10y ago
>I would like my month spent on transitivity of subclassing back :( Oh God, that gave me flashbacks. I've done at least one transitivity of subtyping proof where I actually got the right theorem, then found later in the module that I had to rewrite the whole thing with a graph-theory library supplying some theorems about DAGs/finite posets. It's horrible, and that piece of work still isn't done!