machine learning with lean4

Stream: Is there code for X?

[Asei Inoue]

I know that there have been efforts to apply machine learning to automatic theorem proving.

Conversely, have any attempts been made to implement machine learning algorithms in Lean4? To what extent has the field of mathematical optimization been formalized in Lean?

[Yaël Dillies]

Have you looked at #Machine Learning for Theorem Proving ?

[Johan Commelin]

I think Asei is asking about the "converse", which isn't much discussed in that stream.

[Johan Commelin]

There is https://github.com/dselsam/certigrad but that's Lean 2.

[Rémy Degenne]

It's not Lean, but this library might interest you: https://github.com/IBM/FormalML

About optimization more specifically than ML in general, in Lean we have the Hahn-Banach separation theorem, which is one of the main tools needed for convex optimization theory, the formulation of dual optimization problems, strong duality, etc. We also have results about convex functions, but I think we don't have much about convex optimization and we don't have anything about particular optimization algorithms. You won't find a proof of convergence of stochastic gradient descent in mathlib, for example.

I am interested in this, but my formalization efforts have been focused on the "stochastic" part of "stochastic gradient descent": a lot of ML is about optimizing models with stochastic algorithms and/or in a stochastic environment, and to formalize that you need some probability.

[Alex J. Best]

Back in lean 3 there was also https://github.com/jtristan/stump-learnable

[Asei Inoue]

Why don't those libraries exist in lean4? Have they decided that it is not worth to be ported?

[Scott Morrison]

Lean 4 is still pretty new!

[Alex J. Best]

Also these lean projects seemed to be for the most part one off research projects, and perhaps not completely polished or seeing wide use, the original authors moved on to other things years ago in some cases. You'd have to ask them if they planned to continue, but nobody in the community decided to maintain or port them

[Asei Inoue]

I found https://github.com/lecopivo/SciLean.