I started theorem proving by computer back in 2017. Back then, there were many working proof assistants in place, but I stumbled on the area by chance and the place where I was at only had a rudimentary implementation. The challenge and awe of working with those tools attracted me to the field. Recent years have made theorem proving more widely available and approachable. In this (incremental) note I will try to put myself in my 2017 shoes to try to decipher the reasons behind this re-emergence.

Writing freshly after the resolution of Navier-Stokes equation's conjecture it is clear that large language models have an important role in this phenomenon. Such achievements although not absent in symbolic theorem proving methods (e.g. the proof of the Robbin's conjecture) did not have the scale that we are currently seeing in mathematician's practice. A reading of the informed literature suggests the construction of proving models based on training on existing corpora of formal proofs. For the theorem proving community, I think this opens the question of theorem proving algorithms that make mistakes, a taboo that is already mentionned by Turing in 1948.