4 ms·

I'm not so certain. Fully automated theorem proving in powerful logics like Coq uses is extraordinarily hard and expensive (between "P=NP" and "halting problem"

by cmrx64 10y ago

I'm not so certain. Fully automated theorem proving in powerful logics like Coq uses is extraordinarily hard and expensive (between "P=NP" and "halting problem" levels of hard and expensive). "Tree search with heuristics" is a very naive way to put it. Tools like Lean will help close that gap, with closer integration with ATPs. But Isabelle has already had great integration with ATPs for a long time now, and while it certainly helps, I don't think we're anywhere near the automated mathematician yet. Creating specific systems which are "easy" to reason about with custom tactics is state-of-the-art, and will probably remain that way for some time. As an aside, http://www.neural-symbolic.org/ http://www.neural-symbolic.org/ is something I watch very closely, and it sounds like you'd be interested in it too!

nickpsecurity 10y ago
The reason is this is an activity centered really on humans understanding a problem and creatively modeling it in new ways until a solution can be made in their logics. The latter part is where much of the automation is helping us. Far as Isabelle and automated provers, I discovered another one recently on that: https://pdfs.semanticscholar.org/a72a/066027389e7745f5ea1cc79aab2163191c59.pdf https://pdfs.semanticscholar.org/a72a/066027389e7745f5ea1cc7... It's probably going to stay like that with human work doing the part requiring real understanding, machines doing the brainless explorations they're good at, and libraries piling up for all the common stuff like what we're seeing a little with Coq and Isabelle/HOL. Btw, your project just came up on Lobsters. I can send you an invite if you want to tell them about it. Right now, nobody is looking at it though which could just be due to time of day. Description sounds like you have broader plans than the Nizza-like scheme we discussed previously. https://lobste.rs/s/3jgbh0/this_year_robigalia https://lobste.rs/s/3jgbh0/this_year_robigalia

by cmrx64 10y ago

nickpsecurity 10y ago

The reason is this is an activity centered really on humans understanding a problem and creatively modeling it in new ways until a solution can be made in their logics. The latter part is where much of the automation is helping us. Far as Isabelle and automated provers, I discovered another one recently on that: https://pdfs.semanticscholar.org/a72a/066027389e7745f5ea1cc79aab2163191c59.pdf https://pdfs.semanticscholar.org/a72a/066027389e7745f5ea1cc7... It's probably going to stay like that with human work doing the part requiring real understanding, machines doing the brainless explorations they're good at, and libraries piling up for all the common stuff like what we're seeing a little with Coq and Isabelle/HOL. Btw, your project just came up on Lobsters. I can send you an invite if you want to tell them about it. Right now, nobody is looking at it though which could just be due to time of day. Description sounds like you have broader plans than the Nizza-like scheme we discussed previously. https://lobste.rs/s/3jgbh0/this_year_robigalia https://lobste.rs/s/3jgbh0/this_year_robigalia