Long PDE or probability papers can reportedly be formalized in 24–48 hours

A user claims long PDE or probability papers can be formalized in 24–48 hours, even with many prerequisites likely absent from mathlib. They say harder projects can take longer, and that they wrote a blog post explaining their approach and are making their Lean skill files public.