Articles by baruchel
22

50 years of proof assistants (lawrencecpaulson.github.io)

3

50 Years of Proof Assistants (lawrencecpaulson.github.io)

1

New Font Release: Bhs (fsd.it)

1

The Little Theorems (computationalcomplexity.org)

16

Set theory with types (lawrencecpaulson.github.io)

3

A New Bridge Links the Math of Infinity to Computer Science (quantamagazine.org)

1

To Have Machines Make Math Proofs, Turn Them into a Puzzle (quantamagazine.org)

21

Steven Heller's Font of the Month: Archive Matrix (ilovetypography.com)

76

Why don't you use dependent types? (lawrencecpaulson.github.io)

3

What Is the Funniest Number? (futilitycloset.com)

2

Terence Tao on non-monotonicity in research (mathstodon.xyz)

26

Mathematicians discover prime number pattern in fractal chaos (scientificamerican.com)

2

Terence Tao on Crowdsourced Effort (mathstodon.xyz)

1

Clyde Kruskal talks about his Father Martin on Martin's 100th birthday (computationalcomplexity.org)

3

New Math Revives Geometry's Oldest Problems (quantamagazine.org)

57

A simple way to measure knots has come unraveled (quantamagazine.org)

3

The Quest to Find the Longest-Running Simple Computer Program (wired.com)

3

Self-Assembly Gets Automated in Reverse of 'Game of Life' (quantamagazine.org)

21

New knot theory discovery overturns long-held mathematical assumption (scientificamerican.com)

24

Lisp Still Matters (funcall.blogspot.com)

4

What Happens When a Scientific Field Changes Its Mind – Scientific American (scientificamerican.com)

4

'It's a Mess': A Brain-Bending Trip to Quantum Theory's 100th Birthday Party (quantamagazine.org)

2

How Can Math Protect Our Data? (quantamagazine.org)

55

Breaking the sorting barrier for directed single-source shortest paths (quantamagazine.org)

3

Some thoughts on journals, refereeing, and the P vs. NP problem (computationalcomplexity.org)

119

At 17, Hannah Cairo solved a major math mystery (quantamagazine.org)

3

Tetris Presents Math Problems Even Computers Can't Solve – Scientific American (scientificamerican.com)

1

A 'Grand Unified Theory' of Math Just Got a Little Bit Closer (wired.com)

1

Why Did the Universe Begin? (quantamagazine.org)

2

Landmark Langlands Proof Advances Grand Unified Theory of Math (scientificamerican.com)

3

A New Geometry for Einstein's Theory of Relativity (quantamagazine.org)

2

Effectively Zero-Knowledge Proofs for NP with No Interaction, No Setup (weizmann.ac.il)

1

For Algorithms, Memory Is a Far More Powerful Resource Than Time (wired.com)

2

The Magic Theorem (aperiodical.com)

1

Computer Scientists Figure Out How to Prove Lies (quantamagazine.org)

6

Science Makes the U.S. a Great Nation (scientificamerican.com)

1

Scientists just simulated the "impossible" – fault-tolerant quantum code cracked (sciencedaily.com)

1

Tom Gauld on an alternative use for unsolved mathematical problems (newscientist.com)

2

Quantum computers just beat classical ones – Exponentially and unconditionally (sciencedaily.com)

29

New proof dramatically compresses space needed for computation (scientificamerican.com)

1

How Does Graph Theory Shape Our World? (quantamagazine.org)

2

The Distribution of Prime Numbers: A Geometrical Perspective (computationalcomplexity.org)

1

Quantum dice: Scientists harness true randomness from entangled photons (sciencedaily.com)

18

Is mathematics mostly chaos or mostly order? (quantamagazine.org)

1

André Seznec Receives the 2025 ACM-IEEE CS Eckert-Mauchly Award (acm.org)

3

There's no cheating this random number generator (sciencenews.org)

7

IBM to build first large-scale, error-corrected quantum computer by 2028 (technologyreview.com)

1

New Quantum Algorithm Factors Numbers with One Qubit (quantamagazine.org)

42

The new Gödel Prize winner tastes great and is less filling (computationalcomplexity.org)

1

Platform for Formalizing Sequences from Online Encyclopedia of Integer Sequences (provables.github.io)

1

Quantum Universe (scientificamerican.com)

2

The Core of Fermat's Last Theorem Just Got Superpowered (quantamagazine.org)

2

Why You Should Care About Functional Programming (borkar.substack.com)

47

Dimension 126 Contains Twisted Shapes, Mathematicians Prove (quantamagazine.org)

2

Rocq 9.0.0 (rocq-prover.org)

3

Boris Spassky (1937-2025) Chess World Champion and Legendary Grandmaster (europechess.org)

4

Lambda Calculus and Lisp, part 2 (recursion excursion) (babbagefiles.xyz)

30

Lambda Calculus and Lisp, part 1 (babbagefiles.xyz)

1

When is it worth the time and effort to verify a proof FORMALLY? (computationalcomplexity.org)

1

Thinking Big (futilitycloset.com)