Aaronson has worked for OpenAI and probably has stock options. Gowers is funded by the "AI for math" fund by XTX markets.

The students who have been alarmed outside his office should take a course in marketing and journalistic ethics to assess the situation more rationally and figure out that the problem might sit in the office.

It is interesting by the way that Google does use Lean in a loop to refine proofs. This was called heresy by AI boosters earlier who said that Lean was never used in proofs.