Commit 2025-10-02 20:11 3c14b55b
View on Github →doc(Logic): update library note [fact non-instances] (#30125) Going through all library notes I noticed that this note still refers Lean 3's instance search mechanisms. Instance synthesis is still not a good proof search mechanism, but it's smarter than before and looks at more than the head symbol now.