Harmonic, Axiom, Math Inc, Axiomatic AI, and others — all companies whose mission includes, in some form, the goal of AI for formalization.

Having spent years formalizing physics, you might expect me to be at the front of the pack cheering these companies on, hoping they succeed and doing everything I can to help. But like many in the formalization community, I find myself generally disappointed with much of what they do and how they act.

Here is the thing: there are a few simple changes these companies could make that would shift my stance entirely. Changes that would put me — and, I suspect, many others in the community — at the front of the pack cheering them on.

So my message to these companies is:

1. Promote the community. Your company likely exists thanks to the hard work of countless volunteers building projects like Mathlib. You should be among the biggest promoters of that community.
2. Support the community. Your company is no doubt good at bringing in money. Use some of it to build infrastructure, fund grants, and recognise members of the community through awards.
3. Be part of the community. Your company likely has many smart people with great ideas about how to formalize different areas. Feed those ideas back. Join the discussions and engage actively. Mathlib and the Lean ecosystem succeed because of open development — support that.
4. Listen to the community. In my opinion, those who hang around the Lean Zulip often have a strong grasp of the bigger picture. Listen to them. If they say, for example, that some code is not going to be maintainable, then it probably isn’t.

Some credit has to be given to Harmonic here, who do make steps in this direction.

Naturally, all of this applies to academics too, and we should hold ourselves to the same standards.