Lawrence Paulson @LawrPaulson Twitter profile

Last Seen Profiles

@AnteCertamen

@RA1005201211

@miz_irritating

@LukeTay79310001

@Mbeyacitycf

@sarinasid

@nadeesha99

@ProlificNorth

@hongfangliu

@puhwint

@ivhan79204921

@michuuuub

@okinomiyaki

@dea_semok

@hisaurabhshah

@chatbiology

@biansbaa

@dorothyforget74

@lunatintaypIuma

@mia_fortuna_

@cgizidro

@makiMseikan

@NYC_DOT

@TwitchItUpRT

@oishiinamako

@DLF_Yvelines

@NwankStefan

@couple705

@Azenda7

@couple705

@Hijabbacol2883

@stw_pdg

@suegrange101

@akira_ca

@armpits81

@__nxde

Lawrence Paulson

@LawrPaulson

5 months

50

4K

44K

Lawrence Paulson

@LawrPaulson

2 years

@jdpoc Turing, with his "Turing machines", created the mathematical field of computation theory. His Bombe helped crack Enigma ciphers. He conceived the idea of artificial intelligence. But he did not invent any sort of computer.

21

6

342

Lawrence Paulson

@LawrPaulson

2 years

@Peston @SuellaBraverman As the grandson of four refugees, I'm acutely aware how wrong it is to demonise some of the world's most vulnerable people. We've had a succession of ministers, themselves descended from refugees, shamelessly indulging in hate out of political expediency. Disgraceful.

9

6

227

Lawrence Paulson

@LawrPaulson

10 months

Donald Knuth's Christmas Lectures now online

Donald Knuth's 2023 Christmas Lecture: Making the Cells Dance

How a "memorable homework" problem from a 1974 computer science book inspired a much more efficient way to sort sets.

thenewstack.io

3

42

183

Lawrence Paulson

@LawrPaulson

2 years

I heard that some students were watching the on-line lectures I recorded during lockdown, so I have uploaded the 12 "Logic & Proof" lectures to my (new) YouTube channel. The first one is here:

5

21

147

Lawrence Paulson

@LawrPaulson

2 years

"I [wanted] meet and to be directed by Alonzo Church. But his much earlier logistic system based on untyped lambda calculus, which he thought was going to solve problems in Frege's system leading to the Russell paradox, had been shown to be inconsistent."

4

33

146

Lawrence Paulson

@LawrPaulson

3 years

@thesundaytimes I bought a house in 1983 for £30K. I was earning £9K and, living in digs, saving for a £3K deposit wasn't hard. Even taking overseas hols. That job today pays maybe £40K. That same house, however, costs half a million.

0

11

137

Lawrence Paulson

@LawrPaulson

8 months

I was recently informed that students were watching recordings that I didn't even know existed: of the last time I delivered the lecture course Logic and Proof, back in 2022. So I edited and uploaded them to Youtube. The quality is poor, but anyway:

Logic and Proof (live version)

These are the 12 lectures of my Cambridge undergraduate course, Logic and Proof, given in 2022. THESE COVER THE SAME MATERIAL as the "Logic and Proof" playli...

www.youtube.com

6

29

145

Lawrence Paulson

@LawrPaulson

2 years

What the actual fuck

7

5

96

Lawrence Paulson

@LawrPaulson

6 months

The Archive of Formal Proofs is about to take off, big time!

5

9

94

Lawrence Paulson

@LawrPaulson

3 years

Lambda-calculus and combinator fans may want to peek at my (1995!) lecture notes:

0

23

90

Lawrence Paulson

@LawrPaulson

3 months

I finally managed to formalise the main result of that Ramsey paper too. (Bhavik got there in November.)

5

3

89

Lawrence Paulson

@LawrPaulson

2 years

@JohnJCrace It’s a crime. Let’s have a prosecution.

1

4

84

Lawrence Paulson

@LawrPaulson

2 years

“By mechanising the WebAssembly formal semantics in Isabelle/HOL … he discovered a number of errors in the specification, drove the adoption of official corrections, and provided the first type soundness proof for the corrected language.”

0

19

77

Lawrence Paulson

@LawrPaulson

5 months

@nycsouthpaw Unbelievable that US citizens are forced to pay a third party just to do their taxes

8

1

78

Lawrence Paulson

@LawrPaulson

2 years

New on my blog: a guest post by Martin Kleppmann. Verifying distributed systems with Isabelle/HOL

0

16

75

Lawrence Paulson

@LawrPaulson

2 years

Q: What is a type? A: A type is a syntactic element of a formal system, endowed (if you are lucky) with semantics. A few words on the history of types here:

8

15

73

Lawrence Paulson

@LawrPaulson

1 year

@AndyGJBurge @Nigel_Farage Who responded to the horrific murder of Jo Cox MP by moaning about its effect on the Leave campaign

Nigel Farage says he’s a victim of political hatred in response to Jo Cox question

Ukip leader admits Labour MP's murder could damage his Brexit campaign

www.independent.co.uk

0

15

69

Lawrence Paulson

@LawrPaulson

3 years

People who are really interested in the lambda calculus also need to check out Dana Scott's riposte to Church and Curry's formalistic outlook.

1

13

67

Lawrence Paulson

@LawrPaulson

2 months

Remembering Michael J. C. Gordon, 28 Feb 1948 – 22 Aug 2017, who did more for interactive theorem proving than practically anybody

Michael John Caldwell Gordon (FRS 1994), 28 February 1948 -- 22 August 2017

Michael Gordon was a pioneer in the field of interactive theorem proving and hardware verification. In the 1970s, he had the vision of formally verifying system designs, proving their correctness...

arxiv.org

4

20

69

Lawrence Paulson

@LawrPaulson

3 years

Types aren't sets; syntax isn't semantics; sets shouldn't be too large.

4

18

63

Lawrence Paulson

@LawrPaulson

1 year

@secrettory12 @johnredwood They definitely argued that only through private ownership could those Victorian sewerage systems be replaced.

3

59

Lawrence Paulson

@LawrPaulson

1 year

People regularly posit set theory and type theory as alternatives, but these have different purposes. 1/3

1

11

59

Lawrence Paulson

@LawrPaulson

7 months

Today is the 20th anniversary of Isabelle's Archive of Formal Proofs. More than 4 million lines. It builds in just over two hours on a parallel machine (actual runtime over 87 hours). This includes slow developments with calculations.

0

17

60

Lawrence Paulson

@LawrPaulson

4 months

I've put my Hausdorff Institute of Mathematics talk on my Youtube channel: Formalising Advanced Mathematics in Isabelle/HOL (HIM will put all the workshop talks on their own channel soon.)

Formalising Advanced Mathematics in Isabelle/HOL

This is a shorter version of "Formalising 21st-Century Mathematics", which was published on this channel in February 2024. I presented this version at the Ha...

www.youtube.com

0

8

39

Lawrence Paulson

@LawrPaulson

2 years

New on my blog: "On Turing machines" (Last week? I was in Corfu.)

1

8

58

Lawrence Paulson

@LawrPaulson

2 years

@davidfrum @DCrittenden1 The advertisements are dismal. Telling people to put their life savings into gold and keep it at home is shockingly bad advice.

2

1

57

Lawrence Paulson

@LawrPaulson

1 year

2

4

53

Lawrence Paulson

@LawrPaulson

4 months

@royalsociety You've gone and triggered the Flat Earthers again. Guys: vaccines work, climate change is real, and by the way your hero Elon is also a Fellow:

6

0

51

Lawrence Paulson

@LawrPaulson

1 year

A 20 minute research talk on formalising material from Apostol's graduate textbook on number theory:

Formalising a Number Theory Textbook: Lessons Learnt

I talk about formalising a graduate-level text on number theory by Apostol in a proof assistant. I show some pages from the textbook along with extracts from...

www.youtube.com

0

12

50

Lawrence Paulson

@LawrPaulson

2 years

A second YouTube playlist, for Interactive Formal Verification. This is an Isabelle course.

0

8

51

Lawrence Paulson

@LawrPaulson

8 months

Isabelle can prove this with a single click. You can break it down into smaller steps if you like

Alex Kontorovich

@AlexKontorovich

8 months

Yep, it checks out! :) (Not that I doubted @wtgowers , of course...) (Only difference: there was an implicit use of injectivity that could have been explicitly mentioned...)

7

8

119

1

8

51

Lawrence Paulson

@LawrPaulson

7 months

RIP Ross Anderson, one of the world's great security researchers

1

6

50

Lawrence Paulson

@LawrPaulson

1 year

@NeilCox139 @thatginamiller What you "think" is worth precisely zero without hard evidence

1

0

51

Lawrence Paulson

@LawrPaulson

1 year

Isabelle2023 is (finally) available! Lots of new stuff

3

11

51

Lawrence Paulson

@LawrPaulson

1 year

4

6

49

Lawrence Paulson

@LawrPaulson

6 months

@Peston Wasn’t it shown at the trial that Rebekah Brooks had shredded quantities of documents the day before the police arrived? But there were no consequences

3

6

49

Lawrence Paulson

@LawrPaulson

2 months

New on my blog: Probabilistic reasoning and formal proof

0

7

52

Lawrence Paulson

@LawrPaulson

2 years

New on my blog: What is the point of formalising mathematics?

2

10

48

Lawrence Paulson

@LawrPaulson

1 year

Set theory emerged from the work of people such as Cantor and Dedekind, aimed at understanding deep issues in topology and the nature of number systems. Most set theorists have no interest in formalising mathematics.

3

46

Lawrence Paulson

@LawrPaulson

9 months

I'm thrilled that somebody has noticed my work! And so soon!!

0

46

Lawrence Paulson

@LawrPaulson

2 years

An OBE for Simon Peyton Jones!

Queen's Birthday Honours 2022

Leaders in fields from chemistry to cancer research are among the Cambridge academics recognised today.

www.cam.ac.uk

0

9

45

Lawrence Paulson

@LawrPaulson

2 years

What is the correct punishment for people who say "PDF format"?

19

1

45

Lawrence Paulson

@LawrPaulson

1 year

New on my blog: What do we mean by "the foundations of mathematics"?

2

11

44

Lawrence Paulson

@LawrPaulson

1 year

Recounting the History of Math’s Transcendental Numbers | Quanta Magazine

Transcendental numbers include famous examples like e and π, but it took mathematicians centuries to understand them.

www.quantamagazine.org

0

13

43

Lawrence Paulson

@LawrPaulson

2 years

@lewis_baston @jdportes What they really want is Belarus-on-Thames

1

0

37

Lawrence Paulson

@LawrPaulson

11 months

@thatginamiller Our government will soon announce a scheme to use sewage as a reliable food source for the poor

7

2

40

Lawrence Paulson

@LawrPaulson

2 years

New on my blog: Formalising Gödel's incompleteness theorems, I

2

11

42

Lawrence Paulson

@LawrPaulson

2 years

@inquiringally @jdpoc It's precisely because I am a Turing fan that I dislike seeing his work misrepresented. You might consider reading the biography by Andrew Hodges, where his achievements are outlined in great detail.

0

40

Lawrence Paulson

@LawrPaulson

2 years

@carolvorders @DanNeidle Isn’t this tax evasion? When will criminal charges brought?

2

3

38

Lawrence Paulson

@LawrPaulson

1 year

@LongFormMath If you really were publishing in Courier, you would deserve this. There was a time when we had to put up with books produced on typewriters. It was 50 years ago.

2

1

39

Lawrence Paulson

@LawrPaulson

1 year

@mathematicsprof If it’s about probability, you can’t beat Great Expectations

2

40

Lawrence Paulson

@LawrPaulson

1 year

@NeilCox139 @thatginamiller No, it's more an objection to people simply making things up

3

0

39

Lawrence Paulson

@LawrPaulson

4 months

@Anthony_Bonato Guess he never read a monograph published in the 1970s, typed and with the formulas written by hand

0

36

Lawrence Paulson

@LawrPaulson

2 years

@PatJHennessy @PickardJE He wasn’t wrong. And his memo illustrated what he wanted.

1

0

36

Lawrence Paulson

@LawrPaulson

1 year

New on my blog: Propositions as types: explained (and debunked)

4

7

37

Lawrence Paulson

@LawrPaulson

2 years

Isabelle 2022 is out!

1

10

36

Lawrence Paulson

@LawrPaulson

1 year

Type theory was introduced by Russell and Whitehead in 1910 for the purpose of formalising mathematics, for which it has been used ever since.

2

1

35

Lawrence Paulson

@LawrPaulson

5 months

@BadMedicalTakes Sam is correct. And 95% of the blind are just people who’re behind in seeing.

1

33

Lawrence Paulson

@LawrPaulson

2 years

New on my blog: "The formalisation of nonstandard analysis"

1

6

34

Lawrence Paulson

@LawrPaulson

1 year

Uniqueness of the fixed point of a contraction map for an abstract metric space, proved by a single Sledgehammer call

2

5

34

Lawrence Paulson

@LawrPaulson

1 year

@Anthony_Bonato Not to be confused with Erdős either. Practice saying Erdős with the correct Hungarian pronunciation

1

2

34

Lawrence Paulson

@LawrPaulson

2 years

New on Machine Logic: why are you being constructive?

7

11

33

Lawrence Paulson

@LawrPaulson

3 years

What's the story of Isabelle's sledgehammer? Find out here.

0

7

32

Lawrence Paulson

@LawrPaulson

1 year

@kimdayers Definitions are choices, not facts. It’s convenient to have zero.

2

0

32

Lawrence Paulson

@LawrPaulson

1 year

@bdlatt @AuschwitzMuseum Yet another person proving that he doesn’t actually read the Auschwitz Memorial posts. Try it, you might learn something

0

31

Lawrence Paulson

@LawrPaulson

2 years

New on my blog: Verifying cryptographic protocols, I: Fundamentals

1

8

31

Lawrence Paulson

@LawrPaulson

1 year

Large-Scale Formal Proof for the Working Mathematician – Lessons learnt from ALEXANDRIA

Large-Scale Formal Proof for the Working Mathematician -- Lessons...

ALEXANDRIA is an ERC-funded project that started in 2017, with the aim of bringing formal verification to mathematics. The past six years have seen great strides in the formalisation of...

arxiv.org

1

8

32

Lawrence Paulson

@LawrPaulson

2 years

80 pages of the journal Experimental Mathematics devoted to formalisations of cool (and not so cool!) results in Isabelle/HOL and Lean

Experimental Mathematics

Volume 31, Issue 2 of Experimental Mathematics

www.tandfonline.com

0

3

31

Lawrence Paulson

@LawrPaulson

2 years

Our paper on formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions — finally!

Formalising Szemerédi's Regularity Lemma and Roth's...

We have formalised Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions, two major results in extremal graph theory and additive combinatorics, using the proof assistant...

arxiv.org

3

9

32

Lawrence Paulson

@LawrPaulson

2 years

New on my blog Martin-Löf type theory in Isabelle: formalisation

0

14

30

Lawrence Paulson

@LawrPaulson

2 years

The same, as outlined in the Tractatus

4

6

30

Lawrence Paulson

@LawrPaulson

1 year

New on my blog: When is a computer proof a proof?

1

7

30

Lawrence Paulson

@LawrPaulson

1 year

New on my blog: Hao Wang on the formalisation of mathematics

3

6

29

Lawrence Paulson

@LawrPaulson

3 months

A cool project done in Coq. And your reminder that it's mathematics, not physics, where you find properly large numbers

Amateur Mathematicians Find Fifth ‘Busy Beaver’ Turing Machine | Quanta Magazine

After decades of uncertainty, a motley team of programmers has proved precisely how complicated simple computer programs can get.

www.quantamagazine.org

1

5

30

Lawrence Paulson

@LawrPaulson

2 years

Hard to argue with this

1

2

27

Lawrence Paulson

@LawrPaulson

2 years

"Alan Turing had been a PhD student of Church before WWII and he insisted that Turing formulate all of his work on transfinite computation in terms of lambda calculus. In one of his letters Turing said how much he hated to do that, but it was what he had to do to finish his PhD."

2

3

28

Lawrence Paulson

@LawrPaulson

2 years

New on my blog: The semantics of a simple functional language

1

3

29

Lawrence Paulson

@LawrPaulson

2 years

We at Cambridge were moved to MS Exchange. It's astonishingly broken. Had to involve an MS engineer to try to figure out why one bad msg header could make the entire spam quarantine page fail. He couldn't. And MS is the "industry leader".

2

4

27

Lawrence Paulson

@LawrPaulson

5 months

@AuschwitzMuseum The survival of even one was a miracle

0

29

Lawrence Paulson

@LawrPaulson

3 years

Type classes versus locales!

2

5

27

Lawrence Paulson

@LawrPaulson

2 years

New on my blog Martin-Löf type theory in Isabelle: examples

1

7

27

Lawrence Paulson

@LawrPaulson

2 years

It is one thing to queue, quite another thing to understand queueing theory

1

5

27

Lawrence Paulson

@LawrPaulson

2 years

Church (1940)

3

2

25

Lawrence Paulson

@LawrPaulson

5 months

Isabelle2024 and its Archive of Formal Proofs are now available. See

0

7

27

Lawrence Paulson

@LawrPaulson

8 months

My LMS/BCS-FACS seminar is now available on my personal Youtube channel too. Many thanks to the organisers for sharing this video!

Formalising 21st-Century Mathematics

My LMS/BCS-FACS Seminar given on 15 January 2024. This is exactly the same recording as the one by the same name on the London Mathematical Society's channel...

www.youtube.com

1

8

27

Lawrence Paulson

@LawrPaulson

2 years

@JDHamkins I did a PhD viva in Edinburgh and was forced to bring my passport to prove that I had the right to work. Because the invading hordes of illegal aliens are fraudulently examining PhD dissertations across the UK

0

27

Lawrence Paulson

@LawrPaulson

2 years

New on my blog: MetiTarski: an automatic prover for real-valued special functions

0

5

25

Lawrence Paulson

@LawrPaulson

2 years

@typeswitch Any cooking tips involving flamethrowers?

1

0

26

Lawrence Paulson

@LawrPaulson

2 years

New on my blog: Formalising a new proof that the square root of two is irrational

1

2

25

Lawrence Paulson

@LawrPaulson

2 years

Can authors please stop describing a machine proof as "straightforward but tedious"? Instead, tell us if you find one that *isn't* tedious

3

0

25

Lawrence Paulson

@LawrPaulson

2 years

It's online! Many thanks to Anthony Bordg for showing that "Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types" [Note: the ePub version is illegible, so go for PDF]

Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types

Church’s simple type theory is often deemed too simple for elaborate mathematical constructions. In particular, doubts were raised whether schemes could be formalized in this setting and a challeng...

www.tandfonline.com

0

6

25

Lawrence Paulson

@LawrPaulson

3 months

@BadMedicalTakes So he’s dead? Then how can he talk?

0

25

Lawrence Paulson

@LawrPaulson

2 years

@EladNehorai Give me a screaming baby any day

0

24

Lawrence Paulson

@LawrPaulson

1 year

New on my blog: The concept of proof within the context of machine mathematics Thanks to @Jose_A_Alonso

0

4

24

Lawrence Paulson

@LawrPaulson

2 years

New on my blog: Memories: Edinburgh ML to Standard ML

2

9

25

Lawrence Paulson

@LawrPaulson

1 year

Regarding "Pearls of Functional Algorithm Design", by Richard Bird. Has anybody formalised any of these derivations, especially the harder ones?

3

2

23

Lawrence Paulson

@LawrPaulson

6 months

"The formal verification of the ctm approach to forcing" An impressive – and very rare – application of Isabelle/ZF

2

6

24

Lawrence Paulson

@LawrPaulson

2 years

Congratulations to Peter!

0

24

Lawrence Paulson

@LawrPaulson

6 months

New in the Archive of Formal Proofs: The Uncertainty Principle, by Alexander Treml A formal proof of the uncertainty principle known from quantum mechanics, based upon work on complex vector spaces .

Uncertainty Principle

www.isa-afp.org

0

3

24