{"id":145,"date":"2025-06-16T22:17:42","date_gmt":"2025-06-16T21:17:42","guid":{"rendered":"https:\/\/blogs.imperial.ac.uk\/parikshit\/?p=145"},"modified":"2025-06-16T22:21:35","modified_gmt":"2025-06-16T21:21:35","slug":"how-i-ended-up-talking-physics-with-a-theorem-prover","status":"publish","type":"post","link":"https:\/\/blogs.imperial.ac.uk\/parikshit\/2025\/06\/16\/how-i-ended-up-talking-physics-with-a-theorem-prover\/","title":{"rendered":"How I Ended Up Talking Physics with a Theorem Prover"},"content":{"rendered":"

I came across a LinkedIn post by a postdoctoral researcher working on something interesting. The first thing that caught my eye was his list of research interests. I always thought someone should focus on one specific domain like biology or physics and explore subfields within that. But this researcher was working at the intersection of mathematics, physics, and computer science.<\/span><\/p>\n

That one word “intersection” clicked something in me. I realized it was possible to combine different interests in a meaningful way. I messaged him on LinkedIn, not really expecting a reply. After all, I was an undergrad from a different background, and he must have gotten a lot of messages. But to my surprise, he responded within minutes.<\/span><\/p>\n

We scheduled a Zoom call for March 27th, 2025, and though I was excited, I had no clue what \u201cLean\u201d was, or what \u201ctheorem proving\u201d meant. I asked a few friends studying physics at Imperial to explain, and after some Googling, it started to make sense.<\/span><\/p>\n

So, What Is Lean and Theorem Proving?<\/b><\/p>\n

Let me explain it the way it started to make sense to me.<\/span><\/p>\n

Take something simple:<\/span><\/p>\n

\u201cEvery time I flip this switch, the light turns on.\u201d<\/span><\/i><\/p>\n

In everyday life, we\u2019d just accept that as true. We\u2019ve seen it happen. But a theorem prover\u00a0 like Lean\u00a0 doesn\u2019t take your word for it.<\/span><\/p>\n

It\u2019s like a robot that says:<\/span><\/p>\n

\u201cProve it. Show me the wiring, the power source, the bulb, the laws of electricity. No skipping.\u201d<\/span><\/i><\/p>\n

If you can explain every single logical step, it\u2019ll say:<\/span><\/p>\n

\u201cYes, this is probably true.\u201d<\/span><\/i><\/p>\n

But if something\u2019s missing:<\/span><\/p>\n

\u201cNope. Try again.\u201d<\/span><\/i><\/p>\n

It feels like overkill at first. But it starts to make sense when you think about systems where guessing or assuming just isn\u2019t good enough.<\/span><\/p>\n

Where Is This Actually Used?<\/b><\/p>\n

Imagine the light switch isn\u2019t just in your bedroom, it\u2019s a switch on a rocket.<\/span><\/p>\n