Currently, when derive := True, the oeis attribute attempts to prove theorems based on the values it computes from the declaration. This has two shortcomings: 1) it necessitates that the declaration is computable (i.e., it cannot support noncomputable def's) and 2) it could result in proving theorems about the wrong values. Instead of computing the values from the declaration, we should change the behavior to look up the values from the OEIS itself. This should relieve both pain points 1) and 2).
Currently, when derive := True, the oeis attribute attempts to prove theorems based on the values it computes from the declaration. This has two shortcomings: 1) it necessitates that the declaration is computable (i.e., it cannot support noncomputable def's) and 2) it could result in proving theorems about the wrong values. Instead of computing the values from the declaration, we should change the behavior to look up the values from the OEIS itself. This should relieve both pain points 1) and 2).