Sure, use whatever method of learning that works well for you.
All I'm saying is that you're unlikely to be making effective use of a tool like this without understanding it's theoretical foundations.
All I'm saying is that you're unlikely to be making effective use of a tool like this without understanding it's theoretical foundations.
Compactness[1] is a useful property of some sets. It’s an example of the type of thing you might want to prove or disprove (eg that a certain set in a given metric space is or isn’t compact, or prove the Heine-Borel theorem or whatever), but if you’re not trying to do that, you can go about your merry way and learn a ton of lean without being aware that the concept of compactness even exists.
The same is true of incompleteness for example, which has literally never entered into the realm of being relevant for anything I’ve done in lean, and is definitely not in any way important prerequisite knowledge.
[1] And yes, I really do know what compactness is and I learned that the hard way by working on a bunch of proofs in analysis. There’s really no substitute for learning by doing. A set S is compact if and only if any open cover (ie family of open sets {T_i}_{i in I} such that the union U_{i in I} T_i is a superset of S for some possibly infinite indexing set I) contains a _finite_ subcover (a family {T_j}_{j in J} where J is a finite subset of I and the union over J of all the T_j’s also covers S). Compactness in logic is a consequence of compactness in the set-theoretic sense and really has no relevance whatsoever to lean.
I do find it implausible that you'd need the type of background that I had in logic back then, which included the type of stuff mentioned, for doing stuff in Lean though.
If you want to master it and use it effectively for something real, yeah some reading would help.
Math is full of fun overloads like this.
Most of my lean work involves software verification and transition systems. I suspect most people here would be interested in software verification rather than trying to solve unsolved math problems. You'd have a frustrating experience without the required logic background, from my experience dealing with a collaborator's new PhD students.
If someone would figure this out, the theoretical advancements they would discover on the way would likely earn them a Turing award.