library_search&relation between lean4 and machine learning

Stream: lean4

[Langze YE]

Hello, I am almost new to lean. I have tried some mathematical proof with lean4. I am interested in "library_search", could someone tell me the principle of "library_search", when and for which questions it can work?(only maths questions?) What's more, I want to learn something of lean about machine learning.For example, I have heard that we can use lean4 can formalized linear regression algorithm, but I don't know how to write the code and why it will be helpful for machine learning. Could someone just give me a simple code or just explain something about the relation between lean4 and machine learning. Thank you!

[Scott Morrison]

The library search tactic has actually been renamed to exact? in current Mathlib. (That is, it is a tactic for asking: "how can I solve this goal use exact <term>.)

It is fairly simple in scope: it tries calling apply on the goal with every declaration in the library (there is some clever indexing here to only try feasible declarations). For any declaration that successfully applies to the goal, we then use "backwards reasoning" (in particular, the solve_by_elim) tactic to try to discharge any subgoals by recursively applying hypotheses from the local context.

[Scott Morrison]

For learning about the connections between Lean4 and machine learning, I suggest you spend a day reading the Machine Learning for Theorem Proving stream.