In a recent talk titled "AlphaProof: From the lab into your hands" at the Mathematics in the Age of Automated Proofs symposium, Deepmind team member Thomas Hubert talked about their AlphaProof tool and said:

We are really working hard to try to actually make this available to all academics for free.

This resolves YES if AlphaProof is available for free to >90% of academics or >90% of members of the Lean Zulip forum. I will require an affirmative case: If for example, there is free availability guarded by a waitlist, then there must be confirming evidence that 90% of people who joined the waitlist have gotten access.