For one thing, the RAM model isn't fine-grained equivalent to MTTM (an example is https://en.wikipedia.org/wiki/Counting_sort which is linear-time on RAM but not MTTM). So, the result might not be the same. But also, Mathlib lacks a RAM machine implementation. So any proof would rest on a custom definition stack which would make it difficult to audit.
alt Hacker News
For one thing, the RAM model isn't fine-grained equivalent to MTTM (an example is https://en.wikipedia.org/wiki/Counting_sort which is linear-time on RAM but not MTTM). So, the result might not be the same. But also, Mathlib lacks a RAM machine implementation. So any proof would rest on a custom definition stack which would make it difficult to audit.