I also enjoy creating proofs as a hobby. When I'm doing it for fun, I tend to use Metamath, in particular, the "Metamath Proof Explorer" (MPE, aka set.mm) which formalizes the most common mathematical foundation (classical logic + ZFC). You can see that here: http://us.metamath.org/mpeuni/mmset.html

Here's a short video intro about MPE that I made: https://www.youtube.com/watch?v=8WH4Rd4UKGE

The thing I like about Metamath is that every step is directly visible. Coq, in contrast, shows "how to write a program to find a proof" - and not the proof itself. So you can see absolutely every step, and follow the details using simple hyperlinks.

Of course, all approaches have pros and cons. Metamath has some automation; the metamath and mmj2 programs can automatically determine some things, and there's been some experiments with machine learning that are promising. However, Coq has more automation, in part because it operates at a different level.

I've done a bit of work on a "next generation" Metamath, Ghilbert[1], but have come to the conclusion that it's too ambitious to do as a part-time project. People might find it interesting, though, because it attempts to take interactivity to a higher level than Metamath, and is (imho) a cleaner language.

[1] http://ghilbert.org/

Hey glad to find someone involved in metamath related project.

I guess if I could simplify my discussion to one question, it would be: Does metamath or ghilbert use a logic inference engine to automate parts of a proof?

The way I understand metamath (the website, not the language) is that it's like an encyclopedia of mathematical knowledge. The encyclopedia is in the form of theorems, lemmas, corollaries, and their proof. But unlike an encyclopedia or disconnected articles, all the propositions build on top of one another. As a result, it builds (or tries to build) the whole mathematical edifice starting from core axioms (well, I guess it didn't build itself, but hundreds of mathematicians contributed to the database, like people contributing to wikipedia in the form of article-writing. As to how automated this process is, I don't know).

Now the question is, can we use this edifice as a database, to be input to a logic inference engine. What this would accomplish is that:

- If I make a query about a mathematical proposition (e.g., Are there infinite prime numbers), the logic inference engine would use the database to conclude that there are if it is able to access all the relevant propositions.

- If it's not able to reach a conclusion, e.g., if my query was "Are there infinite twin primes?" it would start a process of exploring new propositions from old propositions. Then either the search would conclude very quickly (if the proposition is only one or two steps away from the knowledge in the database) or it would give up after a few million, or billion attempts (e.g., this is more likely the case with the twin prime query). There will have to be a manually-specified cutoff point otherwise it could go into an infinite loop (I guess it may have something to do with decidability, incompleteness theorem, halting problem, etc, etc. Though even many decidable problems are computationally intractable due to very very large search space).

- Suffice to say, when I say "query" I don't mean a question in english language but a well-crafted mathematical statement in language of metamath itself.

P.S.: As for your mention of this work not doable as part-time, I fully agree with you. It would have enough cognitive load to be a very complex project even if done full time.

Metamath basically goes in the other direction than most proof assistants, it relies on human ingenuity. There is a bit of search in the original C metamath (the "improve" feature) and also just a tiny amount in mmj2 (unification), but if the user doesn't have a clear picture what the fine-grained steps are, they're going to have a bad time.

One of the interesting things about Metamath is that proofs tend to be very concise. In more automated proof systems, you use automated tactics and proof search techniques, and if you expanded out their output, they'd generally be quite verbose. I think this has led a lot of people to believe that automation is more necessary than it actually is.

All that said, you absolutely could build an inference engine of similar scope as the other big proof assistants, and use the existing Metamath database as a rich foundation.

Happy to answer other questions.

These notions are actually becoming more and more intermixed. You could say today that interactive theorem proving (what is done in a proof assistant) is an extension of automated theorem proving, as for example the Isabelle proof assistant has very strong support for proving intermediate theorems automatically.

Thanks, I think this is a good example of what I'm looking for.

One key ingredient is the presence of a logic inference engine (and not for type inference only, as in Coq, Haskell).

- If your system doesn't have a logic inference engine, it's a vanilla proof-assistant (Coq).

- If it has one, it's one of two:

  - a partially-automated theorem prover, (Isabelle)

  - a fully-automated theorem prover

P.S.: Wait a minute. It just occurred to me, is Coq using its Hindley-Milner Type Inference engine as a Logic Inference engine for verifying constructed proofs of theorems and propositions? (is that the killer idea?)