Submissions from lawrencecpaulson.github.io

		How I came to write that paper with Leslie Lamport (lawrencecpaulson.github.io)
		58 points by baruchel 34 days ago \| past \| 11 comments
		Why is it all in the kernel? (lawrencecpaulson.github.io)
		1 point by vinhnx 52 days ago \| past \| 1 comment
		Why is it all in the kernel? (lawrencecpaulson.github.io)
		87 points by ibobev 55 days ago \| past \| 39 comments
		Mizar: The first usable proof assistant for mathematics (lawrencecpaulson.github.io)
		3 points by danielam 72 days ago \| past
		The Dottie Number (lawrencecpaulson.github.io)
		4 points by ibobev 3 months ago \| past
		Nullius in verba: the motto of the Royal Society (lawrencecpaulson.github.io)
		2 points by ibobev 3 months ago \| past
		50 Years of Proof Assistants (lawrencecpaulson.github.io)
		2 points by tosh 4 months ago \| past
		Mizar: The first usable proof assistant for mathematics (lawrencecpaulson.github.io)
		2 points by ibobev 4 months ago \| past
		Mizar: The first usable proof assistant for mathematics (lawrencecpaulson.github.io)
		5 points by chmaynard 4 months ago \| past
		“Why not just use Lean?” (lawrencecpaulson.github.io)
		304 points by ibobev 5 months ago \| past \| 209 comments
		Why Not Use Lean? (lawrencecpaulson.github.io)
		7 points by sebg 5 months ago \| past
		Why Not Use Lean? (lawrencecpaulson.github.io)
		6 points by baruchel 5 months ago \| past
		Memories: Doing my PhD at Stanford, under John L Hennessy (lawrencecpaulson.github.io)
		2 points by ibobev 7 months ago \| past
		Memories: Doing my PhD at Stanford, under John L Hennessy (lawrencecpaulson.github.io)
		1 point by chmaynard 7 months ago \| past
		Broken Proofs and Broken Provers (lawrencecpaulson.github.io)
		64 points by RebelPotato 7 months ago \| past \| 14 comments
		Broken Proofs and Broken Provers (lawrencecpaulson.github.io)
		2 points by ibobev 8 months ago \| past
		50 Years of Proof Assistants (lawrencecpaulson.github.io)
		1 point by thunderbong 9 months ago \| past
		50 years of proof assistants (lawrencecpaulson.github.io)
		144 points by baruchel 9 months ago \| past \| 30 comments
		Finish Your Degree (lawrencecpaulson.github.io)
		3 points by sebg 10 months ago \| past
		Mike Gordon and hardware verification (2023) (lawrencecpaulson.github.io)
		12 points by sebg 10 months ago \| past
		Set theory with types (lawrencecpaulson.github.io)
		125 points by baruchel 10 months ago \| past \| 19 comments
		Set Theory with Types (lawrencecpaulson.github.io)
		6 points by ibobev 10 months ago \| past \| 1 comment
		Why don't you use dependent types? (lawrencecpaulson.github.io)
		269 points by baruchel 10 months ago \| past \| 116 comments
		Everything you know is wrong (lawrencecpaulson.github.io)
		5 points by mrw34 on Sept 20, 2025 \| past \| 1 comment
		Program verification is not all-or-nothing (lawrencecpaulson.github.io)
		1 point by tempodox on Sept 13, 2025 \| past
		Program verification is not all-or-nothing (lawrencecpaulson.github.io)
		3 points by Bogdanp on Sept 11, 2025 \| past
		Memories: Edinburgh ML to Standard ML (lawrencecpaulson.github.io)
		8 points by fanf2 on May 12, 2025 \| 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
		More