Terence Tao: Formalizing a proof in Lean using GitHub Copilot and canonical [video]

Comments (1)

5rest · 7h ago

Terrent Tao's video description: In this experiment, I took a statement in universal algebra that a collaborator of mine (Bruno Le Floch) on the Equational Theories Project had written a one-page human proof of, and set the task of formalizing the proof in a very low-level, "line by line" fashion, with heavy reliance on both the large language model-powered code completion tool "Github Copilot" and the dependent type matching tactic "canonical". The proof was formalized in about 33 minutes.

Plain Vanilla Web (plainvanillaweb.com)

From: Steve Jobs. "Great idea, thank you." (blog.hayman.net)

Void: Open-source Cursor alternative (github.com)

Ty: A fast Python type checker and language server (github.com)

Mozilla Firefox – Official GitHub repo (github.com)

The world could run on older hardware if software optimization was a priority (twitter.com)

The Barbican (arslan.io)

My new deadline: 20 years to give away virtually all my wealth (gatesnotes.com)

ALICE detects the conversion of lead into gold at the LHC (home.cern)

A critical look at MCP (raz.sh)

First American pope elected and will be known as Pope Leo XIV (cnn.com)

LegoGPT: Generating Physically Stable and Buildable Lego (avalovelace1.github.io)

Business books are entertainment, not strategic tools (theorthagonist.substack.com)

Waiting for Postgres 18: Accelerating Disk Reads with Asynchronous I/O (pganalyze.com)

NSF faces shake-up as officials abolish its 37 divisions (science.org)

Leaving Google (airs.com)

I hacked a dating app (and how not to treat a security researcher) (alexschapiro.com)

Vision Now Available in Llama.cpp (github.com)

Reservoir Sampling (samwho.dev)

Ask HN: What are good high-information density UIs (screenshots, apps, sites)?

A simple 16x16 dot animation from simple math rules (tixy.land)

Ask HN: How are you acquiring your first hundred users?

One-Click RCE in Asus's Preinstalled Driver Software (mrbruh.com)

Mistral ships Le Chat – enterprise AI assistant that can run on prem (mistral.ai)

High tariffs become 'real' with our first $36K bill (blog.adafruit.com)

Embeddings are underrated (2024) (technicalwriting.dev)

Car companies are in a billion-dollar software war (insideevs.com)

Observations from people-watching (skincontact.substack.com)

US Copyright Office found AI companies breach copyright. Its boss was fired (theregister.com)

The great displacement is already well underway? (shawnfromportland.substack.com)

Rust’s dependencies are starting to worry me (vincents.dev)

US vs. Google amicus curiae brief of Y Combinator in support of plaintiffs [pdf] (storage.courtlistener.com)

Google is building its own DeX: First look at Android's Desktop Mode (androidauthority.com)

Branch Privilege Injection: Exploiting branch predictor race conditions (comsec.ethz.ch)

Multiple security issues in GNU Screen (openwall.com)

Flattening Rust’s learning curve (corrode.dev)

Bus stops here: Shanghai lets riders design their own routes (sixthtone.com)

Sofie: open-source web based system for automating live TV news production (nrkno.github.io)

I built a native Windows Todo app in pure C (278 KB, no frameworks) (github.com)

Can you trust that permission pop-up on macOS? (wts.dev)

FastVLM: Efficient vision encoding for vision language models (github.com)

RybbitL Open source Google Analytics replacement (github.com)

AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms (deepmind.google)

I ruined my vacation by reverse engineering WSC (blog.es3n1n.eu)

Writing an LLM from scratch, part 13 – attention heads are dumb (gilesthomas.com)

The FTC puts off enforcing its 'click-to-cancel' rule (theverge.com)

Writing that changed how I think about programming languages (bernsteinbear.com)

Gmail to SQLite (github.com)

Mycoria is an open and secure overlay network that connects all participants (mycoria.org)

WASM 2.0 (w3.org)

Terence Tao: Formalizing a proof in Lean using GitHub Copilot and canonical [video]

Comments (1)