[Tainnor]

> Proving things with formal calculi still relies on something like creativity, which itself isn't captured by a precise algorithm, similar to informal proofs.

That's because first-order logic (and any system that extends it) is formally undecidable, so there can be no algorithm that, for a given statement, determines whether it is a valid theorem. If you restrict yourself to propositional logic, you gain decidability but, in the general case, it's still extremely inefficient (unless P=NP).

Of course, in order to prove these things, you have to formally develop what logic is.

[cubefox]

Yeah. Though if one is loose with the word "algorithm" one can count an advanced machine learning model (a few years from now) as such an algorithm. It wouldn't be able to prove or disprove every given first-order statement, but perhaps the vast majority below a certain length. Maybe it could decide every conjecture we are interested in.