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

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