dan on Nostr: it won't on its own write "clean" Lean so you have to tell it to declutter code by ...

it won't on its own write "clean" Lean so you have to tell it to declutter code by showing examples of obnoxious definitions. check out Mathlib and TauCeti locally and tell it to look for what clean Lean code looks like