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.
1,000From Eric Wieser on Zulip:
As many of you know, a key goal for us has been to get AlphaProof into the hands of mathematicians. We are also excited to share an update on this front.
We have now developed a VSCode extension for interacting with AlphaProof, and as a first step, we are beginning to share it with a small, private group of trusted testers to gather initial feedback. This is a crucial phase that will allow us to iterate quickly and improve the tool before any wider release.
We are still in the very early stages of this process and access remains highly limited. However, for those who are deeply interested in providing early feedback and helping to shape the tool's future, you can register your interest via the form at ...
Please understand that we will only be able to onboard new testers very gradually as we scale up. We appreciate your patience, and are incredibly excited about the journey to making AlphaProof a useful collaborator for the mathematics community.