Hello,
A static check calibrated on known-defective statements (and verified in Lean 4.9)
finds 23 Lean Workbook statements whose big-operator body is unparenthesised, so the
binder variable escapes its scope. Under autoImplicit these elaborate with a phantom
universally quantified variable and do not state the intended mathematics. An example
is a telescoping identity that parses as (sum of (k+1)!) minus a phantom k factorial.
Since the corpus is used as a training reward source, these items pay reward for
proving accidents. Full list, contexts, and the detector script attached on request.
Hello,
A static check calibrated on known-defective statements (and verified in Lean 4.9)
finds 23 Lean Workbook statements whose big-operator body is unparenthesised, so the
binder variable escapes its scope. Under autoImplicit these elaborate with a phantom
universally quantified variable and do not state the intended mathematics. An example
is a telescoping identity that parses as (sum of (k+1)!) minus a phantom k factorial.
Since the corpus is used as a training reward source, these items pay reward for
proving accidents. Full list, contexts, and the detector script attached on request.