I was recently writing up a paper after looking at Lean, and just had a moment where I realized the words I was writing were incredibly imprecise. Somebody working in the field could probably translate what I had written into a formal argument if they bothered, but if it had been an answer in an exam I would have requested many more details.
This has gotten me to think about what the "purpose" of a math paper is. Of course, one wants to prove theorems correctly, but what level of rigor should be acceptable for communication? We are still at a point in time where full Lean verification still requires considerable effort and technical knowledge, and precedent says filling out all the details in a math paper is generally a waste of time for both you and the reviewer. Removing a lot of rigor and unnecessary formalism buys clarity.
When Lurie proved the cobordism hypothesis, it was presented as a sketch and was filled in afterwards by other authors. Papers with lengthy derivations often relegate them to an appendix to improve readability. There are also many anecdotes in the study of automorphic forms and trace formulas where the convergence of integrals is written as a given, but later a separate publication of dozens of pages is required to justify that Last Theorem.
To me the synthesis is, we require rigor to verify the argument is correct. However, verification by another party is expensive. To achieve that end, before AI, we placed the onus of verification on the author by requiring maximal detail to lower the verification burden on the reviewer.
AI changes the assumptions of this system a bit. The cost of verification is going down very fast. If a reviewer is using AI to assist, the total cost of a review goes down significantly but the new marginal cost to verify some left-out details is not large. This sort of setup invites a bit of, to borrow a term from economics, moral hazard, unless standards are set. There isn't a governing body that can enforce these things explicitly, but the community decides these things in a decentralized way.
What are others' thoughts are on whether AI should be allowed to lower the rigor required for mathematics papers, and if so to what extent and manner?