Saying hi

Stream: new members

[Rick de Wolf]

Hi everyone, just wanted to quickly introduce myself! I'm Rick, a MSc student in robotics with an interest in maths and CS. I came across Lean a while ago, and I've got some ideas about building a mathematical knowledgebase using Lean. Currently trying to learn Lean to see if the ideas make any sense :stuck_out_tongue_wink: Would love to hear from people here, especially if you've got a non-maths background as well :grinning_face_with_smiling_eyes:

[Eric Wieser]

Hi RIck! I did a fair amount of robotics and control theory stuff in my MEng; so it sounds like I fall into the "non-maths" background you're looking for.

[Eric Wieser]

I've got some ideas about building a mathematical knowledgebase using Lean.

I assume you're already aware of the rather large mathematical knowledgebase we already have in the form of "mathlib"? You can search it at #docs.

[Eric Wieser]

You might be interested in some of the discussion at #general > Control theory for LTI systems, as I imagine that overlaps with the robotics you've studied.

[Rick de Wolf]

Hiya Eric! Nice to hear from you. I know about mathlib through one of Kevin Buzzard's recorded talks - it seems like a monumental community effort. I'd love to help out with the mathlib4 porting project once I get some solid footing in lean.

The thing I'm interested in finding out is if lean would be suitable in fields other than mathematics, which have a solid basis in maths nonetheless. So physics and engineering for example. Writing down models of physical systems, and physical laws could be interesting. I'm not yet convinced that lean is a good fit for this, but since it is such a rigorous system I feel like science in general could benefit from it.

I've got some other ideas floating through my head as well, but I'll keep things brief here :wink: I'll check out the control theory discussion you linked - it seems like something that'd be a good fit for me!

I'm curious, with your background in engineering, what brought you to lean?

[Eric Wieser]

I'm curious though, with your background in engineering, what brought you to lean?

Here's some slides for a talk that I gave to the information division of my department this time last year, which somewhat answers that question. In essence, I got fed up with making sloppy algebra mistakes, and found sympy wasn't extensible enough to do what I wanted.

[Eric Wieser]

The thing I'm interested in finding out is if lean would be suitable in fields other than mathematics, which have a solid basis in maths nonetheless. So physics and engineering for example. Writing down models of physical systems, and physical laws could be interesting.

#general > Formalizing Chemical Theory pt. 2 is an example of some other users interested in this.

[Rick de Wolf]

That sounds familiar haha Now you definitely have my attention - I'd love to combine the power of a computer algebra system like Sympy with Lean. The CAS that I have in mind is Julia's Symbolics.jl package, but feature support in that package is severely lacking on some fronts. It feels like reimplementing the same things that Sympy has implemented is simply inefficient. So I'm trying to think of a way to write something down once, in Lean, and then having a 'translation' layer that lets Sympy and Symbolics.jl automatically use the Lean implementation. It would cut development time down once it's up and running (if this is possible).

That was a bit of a tangent, but I'll definitely check out your talk! Having some tools that help with straightforward algebraic manipulations would probably be great for engineering students.

[Bulhwi Cha]

Nice to meet you, Rick! I was an undergraduate in aerospace engineering, though I left my university three weeks ago. I've spent most of my time studying mathematics and logic rather than physics and engineering, but I'm interested in formalizing classical mechanics. I wrote about my goals in #new members > Bulhwi Cha & Seongwoo Shim: Introductions.

[Bulhwi Cha]

Sadly, Seongwoo is no longer willing to participate in formalization of classical mechanics. It's up to me to learn about Mathlib APIs and symplectic geometry.

Rick de Wolf said:

I'd love to help out with the mathlib4 porting project once I get some solid footing in lean.

I finished reading "Theorem Proving in Lean 4" last month, and now I'm trying to port data.string.basic and its dependencies. I recommend this book.

[Rick de Wolf]

Hey Bulwhi, nice to meet you! I'll keep an eye for your classical mechanics port, would love to see what you come up with :smiley: And thanks for linking that book, I'll take a look once I'm done with the natural numbers game.

[Tyler Josephson ⚛️]

Hi! Thanks @Eric Wieser for the shout out. I’m an assistant professor in Chemical Engineering, and I and several UG and grad students in my research group are learning Lean. On the theorem proving side, we have a vision for formalizing theories in science and engineering, using Lean not just to ensure the math is correct, but also to link together scientific concepts, as well. On the programming side, we see Lean as valuable for enabling formally correct scientific computing, to ensure that codes for running physics-based simulations are bug-free.

[Tyler Josephson ⚛️]

Also, pointing you to the SciLean project, as well:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/SciLean.3A.20scientific.20computing.20with.20Lean

[Rick de Wolf]

Hi Tyler, nice to hear from you! I love the ideas you're talking about, they sound like a wonderful way to make knowledge more widely available. Is there any material publicly available from the ATOMS lab about the philosophy and general plans? I'd love to have a look sometime.

[Tyler Josephson ⚛️]

Conclusions and outlook from our arxiv paper would be one place with some of our vision. Bug-free programming in Lean was first brought out in the Certigrad paper, which has been some of our inspiration. I can also send you some proposals we're hearing back from, too.

[Tomas Skrivan]

I have similar interests. I'm working on the mentioned library SciLean, my current focus is to bring symbolic and automatic differentiation to Lean. Once it is done we can start building lots of interesting stuff on top of it.

[Rick de Wolf]

That's an interesting angle @Tomas Skrivan. Are you building autodiff and symbolics using pure Lean?

[Rick de Wolf]

Are @ mentions okay on here, by the way?

[Tomas Skrivan]

Rick de Wolf said:

That's an interesting angle Tomas Skrivan. Are you building autodiff and symbolics using pure Lean?

Yes, I'm doing it purely in Lean.