Automating proofs for computability

Stream: mathlib4

[Palalansoukî]

Many proofs involving Computable (or Partrec, Primrec, etc.) are not human-readable like this. Moreover, in many cases, it is possible to derive proofs automatically from the definition of the function (in the first place, any effective function defined in Lean which is not marked as noncomputable would be computable). Therefore, I believe that, similar to Continuous or Measurable, it should be possible to automate proofs using Aesop for computability. Is there a specific reason why such attempts have not been made yet?

[Patrick Massot]

Nobody is working on that corner of Mathlib.

[Patrick Massot]

Feel free to do it.