This is my #Lean 4 #proof of the nonexistence of #God, based on "§2.4 Modeling English Propositions" p.37 of "A Logical Approach to Discrete Mathematics" by Gries and Schneider (1993):

• If God were able and willing to prevent evil, He would do so:
Able ∧ Willing → Prevents
• If God were unable to prevent evil, He would be impotent:
¬Able → Impotent
• If God were unwilling to prevent evil, He would be malevolent:
¬Willing → Malevolent
• God does not prevent evil:
¬Prevents
• If God exists, He is neither impotent nor malevolent:
GodExists → ¬Impotent ∧ ¬Malevolent
• Therefore, God does not exist:
¬GodExists

Shed no tears for me, were I to end up in #Hell. That my code type checks in Lean 4 at all is a little bit of #Heaven for me.

#DependentTypes #ProofAssistants

https://shorturl.at/wbp1V

You don't need a PhD to start writing simple maths proofs in Lean.

This beginner-friendly course gets you started making your first steps.

https://www.amazon.com/dp/B0DWHS1RDJ

#maths #leanprover #proofassistants #lean4

I realise there is a lot of momentum behind Lean for maths proofs.

But I'm also aware of a very established community around Agda.

Can someone explain in plain English - and for a complete beginner like me - what the main benefits of Agda are over Lean?

My own small experience with Lean is not advanced at all, I liked what I tried, but what I didn't like was the arbitrariness of finding tactics for your proof step needs. Does Agda do this better?

To elaborate on that - I found that my ability to write proofs depended very much on my ability to know/find tactics - and they don't seem to be organised in a way that makes finding "what you don't know" easier. And the tactic search engines are still not that easy to get working well (or at all, in my case).

#agda #leanprover #proofassistants

The author of the textbook I'm following has emphasised the importance of a class of judgements include the entailment *:□, that is

\[\Delta; \Gamma \vdash *:\Box\]

He's done this by talking about them a lot, and including them in the exercises a lot. But. he hasn't spelled out why they're important - I guess expected us to work out it.

But I haven't! I'd welcome help...

https://cs.stackexchange.com/questions/175981/importance-of-delta-gamma-vdash-box

#typetheory #lamdacalculus #proofassistants

I've been working through Type Theory & Formal Proof.

Why? I was curious as to how proof assistants like Lean worked. Someone recommended it.

Is it any good? I think the book is excellent. It provides a gentle ramp from no previous knowledge to the basics of lambda calculus and some extensions, and the central idea of propositions as types / proofs as terms. The exercises are well calibrated. Of course nothing is perfect but this is far better than most texts I've suffered through.

I'm self-teaching so there is a chunky risk my errors and misunderstandings go uncaught... but I'm writing up my solutions in case others find them useful. Writing them publicly also pushes up my own quality threshold from scribbles in a notepad to something more thought through.

https://type-theory-and-formal-proof.blogspot.com

#maths #typetheory #lambdacalculus #proofassistants

50 years of proof assistants

https://lawrencecpaulson.github.io//2025/12/05/History_of_Proof_Assistants.html

#HackerNews #50years #ProofAssistants #History #TechInnovation #Education

Where will all the energy and funding go after the AI bubble comes burning and crashing down?

Formal verification.

That's my prediction. ... ok maybe it's a hope.

#ProofAssistants #formalverification

Months ago I dipped my toe into Lean+mathlib as a proof assistant. I wanted to know how it worked. That led me to start learning about "propositions as types" and "inhabitants as proofs"...

I've somehow managed to get to the end of Chapter 7 of Type Theory and Formal Proof - almost half way.

I'm working through all the exercises and writing them up - caution, some may be wrong - but it helps me learn better.

https://type-theory-and-formal-proof.blogspot.com/p/contents.html

#maths #typetheory #ProofAssistants

currently watching

"Is it time for a new proof assistant?"

by @jonmsterling

https://www.youtube.com/watch?v=7oBkEbKJvnE

#ProofAssistants #typetheory