This is the #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

This is the #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

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

50 years of proof assistants

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

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

Have you ever written Agda code in anger? Well now you can come and write Agda code in Angers!

The Agda Implementors’ Meeting XLI will take place in Angers, France from 2025-11-24 to 2025-11-29 (Mon to Sat). We have a very nice venue La Bulle en Bois which includes a coworking place, a vegan & organic canteen, and a fablab with 3d printers and laser cutters!

Registrations are now open on the Agda Wiki at https://wiki.portal.chalmers.se/agda/Main/AIMXLI and there is a soft registration deadline on 24 October. I hope to see many of you there!

#Agda#ProofAssistants#DependentTypes#Angers

Have you ever written Agda code in anger? Well now you can come and write Agda code in Angers!

The Agda Implementors’ Meeting XLI will take place in Angers, France from 2025-11-24 to 2025-11-29 (Mon to Sat). We have a very nice venue La Bulle en Bois which includes a coworking place, a vegan & organic canteen, and a fablab with 3d printers and laser cutters!

Registrations are now open on the Agda Wiki at https://wiki.portal.chalmers.se/agda/Main/AIMXLI and there is a soft registration deadline on 24 October. I hope to see many of you there!

#Agda#ProofAssistants#DependentTypes#Angers