I'm curious if anyone here is able to describe the state of the art in that. Is it really just a toy for basic things right now, or how realistic is it that we'd ever get to a point where the author of a paper like this could use a formal language to show that their proof is indeed valid and complete?
Kepler conjecture was stated in 1611 and had been unsolved since. Thomas Hales started a project to attack it in 1992. After six years of work, he announced the proof in 1998, in the form of 250 pages of argument and 3 gigabytes of computer calculation. He submitted it to Annals of Mathematics, one of the most prestigious math journal, for review. Reviewers and the author tried valiantly for five years, gave up, and published it in 2003 with a warning that while reviewers were 99% certain, it couldn't be completely reviewed.
Soon after getting this both rejection and acceptance, Thomas Hales announced the plan to formalize his proof to remove any uncertainty. It was enthusiastically received by automated theorem proving community. For a while Thomas Hales "shopped" for the prover tool to use and basically leaders of every significant provers tried to "sell" it to him. He decided on HOL Light, wrote the detailed plan for formalization, and estimated it would take 20 years. He actually carried out this plan, announced the completion in 2014, wrote the paper on formalization, and submitted the formalization paper, with 21 collaborators, in 2015. The formalization paper was published in 2017.
So there's that. The formal proof of Kepler conjecture is at the moment the most significant corpus of formalized mathematics in existence.
then
> plan to formalize his proof ... estimated it would take 20 years
so is it just me, or is the "work" of the normal proof only took 1/5th of the time it took for the automated/formalized proof?! that seems counter-productive imho...
Also, as it was all unknown stuff at the time, any estimation would have been made without prior experience.
Formal proof software will help you on small stuff, but you will still do most of the work, and you have to go much more in details, so it takes much more time.
It took 5 times to make it not a hunch but a real demonstration. If that's counterproductive or not remains as a something opinable.
> make it not a hunch
That's not what automation is doing; it doesn't turn conjectures into proofs. It finds mistakes in proofs; those proofs are not "hunches" but rigorous efforts.
Something which finds faults demonstrates is value mainly whenever it finds a fault. (Or at least that is a very easy perception to slide into.)
Note that we now actually know there is no more fault, because formalization is complete.
The first one is proof assistants, such as Isabelle/HOL, HOL Light, HOL4, Coq, PVS, Lean, TLApm (and others). These are typically languages to be used directly by a human, and share many common features with programming languages. In a sense, you "program" your proof. There are some large developments in such languages, as pointed out in other comments, including the Kepler conjecture (in HOL Light), the 4 colors theorem and Feit-Thompson theorem (in Coq), a fully verified micro-kernel (SEL4, in Isabelle/HOL), etc. It's an active research area with multiple teams around the world, but the provers are still difficult to use for non-experts. Isabelle/HOL has some nice features and good documentation that make it a bit more approachable to newcomers, afaik, and Lean has promising design decisions, but clearly right now it's a lot of effort to formalize anything consequent in proof assistants.
The second area is fully automatic provers — an endeavour started very early (50s, 60s?). Such provers accept a logic formula as input, and try to compute if it's a theorem or not. They typically accept more restricted fragments of logic (because it's a super hard problem!). Even first-order logic, which is less expressive (and convenient) than the higher-order logic usual in proof assistants, is semi-decidable only because of Gödel's incompleteness theorem. This means a prover for this logic will never terminate on some inputs that are not theorems. There still are interesting provers for FOL, e.g. [E](https://eprover.org). More restricted fragments that tools can effectively deal with are SAT (purely propositional logic, solvers are very good nowadays) and SMT (SAT + theories such as arithmetic) which is very useful in software verification (e.g. liquid haskell's type system, why3, boogie, F*, etc.).
There are people trying to join both domains of research by developing so-called "hammers", that make automatic provers available in proof assistants to make small proof steps entirely automatic.