is misformalized as "for any Polynomial with name X", not for "the monomial Polynomial.X". With this option on, this now gives an error that X doesn't exist.
The solution is either to add the missing arguments (when the formalization is correct), or fix the formalization (when it is not).
These are a common source of misformalizations. For instance,
https://github.com/trishullab/PutnamBench/blob/a945338fdc523d7612108a1d7fc07602b19cdde4/lean4/src/putnam_2017_b2.lean#L14
has the parenthesization around the summation incorrect, and so
iis not in scope. As another example,https://github.com/trishullab/PutnamBench/blob/a945338fdc523d7612108a1d7fc07602b19cdde4/lean4/src/putnam_1978_a3.lean#L8-L10
is misformalized as "for any
Polynomialwith nameX", not for "the monomialPolynomial.X". With this option on, this now gives an error thatXdoesn't exist.The solution is either to add the missing arguments (when the formalization is correct), or fix the formalization (when it is not).