The number of scams perpetrated against traditional bank account holders doesn't seem to support the suggestion that scammers aren't interested in regular person-sized targets.

So has he hired anyone who does not exist to champion the cause of the innocent and helpless in a world of criminals who operate above the law?

Presumably you could just require % amounts to be specified (and make sure to pick volume vs weight in some fashion that avoids gaming).

Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.

What commercial setting do you want to use a Lean theorem-proving agent in?

Mathematics, Inc [1], I assume

[1] http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD427.PDF

Or, more accurately: it's not possible to apply copyright to generated code; if you don't release it, it's a trade secret, but if you do, people can use it how they please.

Is this effectivly mit or no license?

Effectively public domain.