People working on the Carleson project in Lean have had to cart around all the explicit constants in their proofs, but now it's done, you can do fun things like reduce one of the constants
\[D=2^{100a^2}\]
to a measly
\[D=2^{3a^2}\]
Note that here \(a\) is not small (\(a\geq 4\)(!)), so that these improvements really matter!
If you have a fediverse account, you can quote this note from your own instance. Search https://mathstodon.xyz/users/highergeometer/statuses/114912415579306596 on your instance and quote it. (Note that quoting is not supported in Mastodon.)