I wondered what this should be about.

After all Interactive Theorem Proving is well established and there are great success stories (e.g. Lean Mathlib).

Who needs automatic theorem proving that mimics interactive theorem proving?

After reading the blog posts on the site:

That endeavour is really about understanding what mathematicians do and replace them with an AI.