Legal and Lean

Stream: Program verification

[Vasu Cho]

Has anyone tried formalizing a legal matter with lean4 ?
Could it be possible to implement the program to verify decisions from courts with lean4 program.

[suhr]

None that I have heard of. There is a language for formalizing legal texts though: https://catala-lang.org/

[Vasu Cho]

I haven't heard of this language. Thanks a lot!
What do you think about the impact of lean4 implementation on other industries ?

[Vasu Cho]

I am curious about lean4 stuffs that could be possibly deployed in other fields alongside startups. Do we have someone in our community try applying this to solve other problems that are related with the daily problem (that as an individual can do with no need large amount of funding) ?

[suhr]

Software verification is usually done using Rocq, but it is slowly changing as more libraries are written in Lean.

What do you think about the impact of lean4 implementation on other industries ?

Most industries are not very formalizable, so proof assistants do not have much impact there.

[Vasu Cho]

That means mostly experts are using lean4 shipping an internal tools rather than building the products ?

In my current understanding, there are some projects/startups like Numina, Harmonic building the new models/products with lean4
but after I dig into this language more
It makes me feel good about helping me structuring logics and want to do more proofs but if I want to apply it for the application or use the knowledge from learning lean4 to build my product. I only see the room for new frontier models developments like Harmonic are doing or go hard mode on pure mathematic as a mathematician

Do you have any suggestions on getting quick wins learning lean4 (for a novice software engineer) and what do you see in a future impact of lean4 ?🙏🏻