| | Mizar: The first usable proof assistant for mathematics (lawrencecpaulson.github.io) |
| 4 points by chmaynard 16 hours ago | past | discuss |
|
| | “Why not just use Lean?” (lawrencecpaulson.github.io) |
| 304 points by ibobev 10 days ago | past | 209 comments |
|
| | Why Not Use Lean? (lawrencecpaulson.github.io) |
| 7 points by sebg 14 days ago | past |
|
| | Why Not Use Lean? (lawrencecpaulson.github.io) |
| 6 points by baruchel 14 days ago | past |
|
| | Memories: Doing my PhD at Stanford, under John L Hennessy (lawrencecpaulson.github.io) |
| 2 points by ibobev 79 days ago | past |
|
| | Memories: Doing my PhD at Stanford, under John L Hennessy (lawrencecpaulson.github.io) |
| 1 point by chmaynard 83 days ago | past |
|
| | Broken Proofs and Broken Provers (lawrencecpaulson.github.io) |
| 64 points by RebelPotato 3 months ago | past | 14 comments |
|
| | Broken Proofs and Broken Provers (lawrencecpaulson.github.io) |
| 2 points by ibobev 3 months ago | past |
|
| | 50 Years of Proof Assistants (lawrencecpaulson.github.io) |
| 1 point by thunderbong 4 months ago | past |
|
| | 50 years of proof assistants (lawrencecpaulson.github.io) |
| 144 points by baruchel 4 months ago | past | 30 comments |
|
| | Finish Your Degree (lawrencecpaulson.github.io) |
| 3 points by sebg 5 months ago | past |
|
| | Mike Gordon and hardware verification (2023) (lawrencecpaulson.github.io) |
| 12 points by sebg 5 months ago | past |
|
| | Set theory with types (lawrencecpaulson.github.io) |
| 125 points by baruchel 5 months ago | past | 19 comments |
|
| | Set Theory with Types (lawrencecpaulson.github.io) |
| 6 points by ibobev 5 months ago | past | 1 comment |
|
| | Why don't you use dependent types? (lawrencecpaulson.github.io) |
| 269 points by baruchel 6 months ago | past | 116 comments |
|
| | Everything you know is wrong (lawrencecpaulson.github.io) |
| 5 points by mrw34 7 months ago | past | 1 comment |
|
| | Program verification is not all-or-nothing (lawrencecpaulson.github.io) |
| 1 point by tempodox 7 months ago | past |
|
| | Program verification is not all-or-nothing (lawrencecpaulson.github.io) |
| 3 points by Bogdanp 7 months ago | past |
|
| | Memories: Edinburgh ML to Standard ML (lawrencecpaulson.github.io) |
| 8 points by fanf2 12 months ago | past |
|
| | Revisiting an early critique of formal verification (lawrencecpaulson.github.io) |
| 2 points by scscsc on March 17, 2025 | past |
|
| | Introduction to the λ-Calculus (lawrencecpaulson.github.io) |
| 46 points by matt_d on Sept 30, 2024 | past | 19 comments |
|
| | Two Small Examples by Fields Medallists (lawrencecpaulson.github.io) |
| 2 points by zaik on Feb 28, 2024 | past |
|
| | Propositions as Types: Explained (and Debunked) (lawrencecpaulson.github.io) |
| 4 points by hackandthink on Jan 6, 2024 | past | 1 comment |
|
| | What do we mean by "the foundations of mathematics"? (lawrencecpaulson.github.io) |
| 139 points by JoelMcCracken on Nov 1, 2023 | past | 139 comments |
|
| | The concept of proof within the context of machine mathematics (lawrencecpaulson.github.io) |
| 2 points by chmaynard on Oct 4, 2023 | past |
|
| | Lambda Calculus: Some Models, Some Philosophy [pdf] (lawrencecpaulson.github.io) |
| 4 points by aebtebeten on Aug 31, 2023 | past | 1 comment |
|
| | Types versus sets (and what about categories?) (2022) (lawrencecpaulson.github.io) |
| 101 points by matt_d on Aug 31, 2023 | past | 36 comments |
|
| | Propositions as Types: Explained (and Debunked) (lawrencecpaulson.github.io) |
| 3 points by ykonstant on Aug 23, 2023 | past |
|
| | When is a computer proof a proof? (lawrencecpaulson.github.io) |
| 2 points by furcyd on Aug 9, 2023 | past |
|
| | The ALEXANDRIA Project: What has been accomplished? (lawrencecpaulson.github.io) |
| 2 points by vilhelm_s on April 27, 2023 | past |
|
|
| More |
