lean: Disable autoImplicits

[eric-wieser]

These are a common source of misformalizations. For instance,

PutnamBench/lean4/src/putnam_2017_b2.lean

Line 14 in a945338

(hS : S = fun a k ↦ ∑ i : Fin k, a + i)

has the parenthesization around the summation incorrect, and so i is not in scope. As another example,

PutnamBench/lean4/src/putnam_1978_a3.lean

Lines 8 to 10 in a945338

	theorem putnam_1978_a3
	(p : Polynomial ℝ)
	(hp : p = 2 * (X ^ 6 + 1) + 4 * (X ^ 5 + X) + 3 * (X ^ 4 + X ^ 2) + 5 * X ^ 3)

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).