Gergely Buday (Mar 24 2025 at 08:57): Gergely Buday (Mar 24 2025 at 08:57):What is an efficient strategy of digesting an existing formalisation? E.g. you need permutations, but the permutations theories are long and it is not obvious what do you really need from them. Also, they might treat permutations differently than you really need. Is there a written account on this?
Mathias Fleury (Mar 24 2025 at 09:07):Usually I look at the definitions (and a tutorial if any). If they look fine, I use and let sledgehammer sort out what I need…
Mathias Fleury (Mar 24 2025 at 09:08):and if SH fails, then I start looking with find-theorems for similar things
Last updated: Apr 03 2025 at 20:22 UTC