4 ms·

I agree that there's generally too little results in mathlib and for that matter in any theorem prover, but I didn't think that work on formalizing such stuff (

I agree that there's generally too little results in mathlib and for that matter in any theorem prover, but I didn't think that work on formalizing such stuff (advanced undergrad results / early grad results) is publishable. Was I wrong in this?

zozbot234 3y ago
There's plenty of published papers about newly formalized proofs, even in "undergrad" math. A formal proof development generally brings to light new information about the original proof, both by plugging all potential inaccuracies/missing steps and in being especially easy to refactor, abstracting out common patterns that might be reused elsewhere.