Ask HN: New way of organizing Mathematical Research

Posted by youoy 13 hours ago

Counter2Comment3OpenOriginal

Hi all,

After all of the recent announcements of AI assisted proofs and the reaction of the mathematical community, it is clear the we need new ways of organizing mathematical research.

The current paradigm of submitting a paper to arxiv, and waiting for the review of the community will not scale with AI research. There is a probable outcome where mathematical statements are so easy to proof (compared to some years ago) that arxiv will be floded with AI slop explanations and their associated lean code. It will then be very difficult to find "classical" mathematical proofs.

On the one hand, the community tends to cluster around the impression that mathematics is more than the formal system (one could even argue that Godel settled this question a long time ago). So we should not allow AI mathematics to be synonymous to mathematics.

On the other hand, there is clear mathematical value in proving a longstanding conjecture with AI tools (for example NS), even if it will take time for the community to digest it. However, i think attaching names/corporations to these staments will do a lot of harm to the community. For example there will be very few people willing to clean AI slop for someone else when that person/corporation did not put the effort.

There seems to be a need for a clear separation between AI slop proofs and classical mathematical knowledge. For this, a possible solution is to build a parallel platform from archive, adapted to AI, with manuscripts + lean code generated mainly by AI, that have not been fully digested.

Submissions to this site should be anonymous. That way, if a mathematitian needs to digest an AI slop proof to include it in a wider finished work, they would be doing it for the community, not for the original person thay submitted it. Even if submission are anonymous, one could extract anonymous metrics about personal impact factor (which goes beyond number of submissions) that could be included for job application as a metric of AI mathematical contributions. That way we also incentivice AI work.

The site should also serve as a context layer for mathematical AI harnesses. This would further speed up mathematical research.

I am aware this is not a fully landed idea. I am sharing it so that we can start an open discussion to perfect it and build it as a community.

I am looking forward to hearing your thoughts. Thank you very much in advance.

Comments

Comment by kdavis 12 hours ago

Unfortunately attaching a corporation name to a statement is a large part of the motivation for a company to spend millions on tokens for Lean proofs. It's a marketing/PR spend for them. Without their name attached, the return on investment is far less.

That said there are some efforts in the direction you're suggesting. For example

- [Prove2Me](https://beta.prove2.me) - Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. One creates open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

- [Tau Ceti](https://github.com/TauCetiProject/TauCeti) - An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics

Comment by gus_massa 3 hours ago

The problem is that the administration of the university needs an easy metric to decide promotions. So we are stuck to paper count. It's too easy to game, add citations. Now add journal impact index, quartiles, h-index and whatever is the new fad.

How does your idea provide a nice metric if the submissions are anonymous?

Or in other words, who is going to pay us for this?

Comment by youoy 2 hours ago

Submissions are anonymous to the exterior viewers, but you do them from one account. You can extract impact metrics from that account for job applications