Kernel Reduction Explosion: a surprisingly inefficient computation in Lean 4

Why does "well-founded recursion" sometimes make Lean 4 definitional equality (kernel reduction) very slow?
Try the interactive trace stepper tool here: dwrensha.github.io/kernel-red....
00:00 - reducing decimalDigits function
01:05 - compilation stages and kernel reduction
03:11 - Zulip suggests adding a fuel parameter
04:26 - printing elaborated function bodies
05:07 - a rundown on WellFounded.fix
06:00 - implementing tracing
06:14 - tracing decimalDigits'
07:16 - tracing decimalDigits
08:05 - tracing minus3
09:50 - conclusion

[@tom7]

I think the real thing to fix about Lean is that it should play the explosion sound whenever you use well-founded induction!

[@ster2600]

Suckerpinch Lean content???? 🥺👉👈

[@francescominnocci]

yes please

[@aze4308]

yes pleaseeee

[@oneofvalts]

Gold, real gold. Thank you so much for this videos.

[@zachbattleman6138]

Such a great video! We need more Lean content like this!!

[@luck-xc7dy]

ive never been more confused 😅

[@yyyxyxyxxyyxxy]

time to get my mind BLOWN