RSS

For­mal Proof

TagLast edit: Sep 26, 2021, 10:04 PM by Pablo

A Formal Proof is a finite sequence of steps from axiom(s) or previous derived proof(s) which strictly follow the allowed rules of inference of the mathematical system in which it exists. They are used to establish statements as true within a mathematical framework in a way which can be independently verified with extremely high certainty, with the most reliable flavor of proof being machine-checked proofs generated by proof assistants since they have even less room for human error.

Proofs, Im­pli­ca­tions, and Models

Eliezer YudkowskyOct 30, 2012, 1:02 PM
131 points
218 comments12 min readLW link

Com­pact Proofs of Model Perfor­mance via Mechanis­tic Interpretability

Jun 24, 2024, 7:27 PM
96 points
4 comments8 min readLW link
(arxiv.org)

A List of things I might do with a Proof Oracle

Logan ZoellnerFeb 5, 2023, 6:14 PM
−14 points
13 comments3 min readLW link

Most Minds are Irrational

DavidmanheimDec 10, 2024, 9:36 AM
17 points
4 comments10 min readLW link

[Question] What Pro­gram­ming Lan­guage Char­ac­ter­is­tics Would Allow Prov­ably Safe AI?

DavidmanheimAug 28, 2019, 10:46 AM
4 points
9 comments1 min readLW link

AXRP Epi­sode 40 - Ja­son Gross on Com­pact Proofs and Interpretability

DanielFilanMar 28, 2025, 6:40 PM
22 points
0 comments89 min readLW link

Squeez­ing foun­da­tions re­search as­sis­tance out of for­mal logic nar­row AI.

Donald HobsonMar 8, 2023, 9:38 AM
16 points
1 comment2 min readLW link

Eleuther re­leases Llemma: An Open Lan­guage Model For Mathematics

mako yassOct 17, 2023, 8:03 PM
22 points
0 comments1 min readLW link
(blog.eleuther.ai)

Davi­dad’s Bold Plan for Align­ment: An In-Depth Explanation

Apr 19, 2023, 4:09 PM
168 points
40 comments21 min readLW link2 reviews

For­mal Proof: O(n) Is a Cog­ni­tive Illusion

Daniil StrizhovMar 28, 2025, 6:26 PM
0 points
0 comments38 min readLW link

Roadmap for a col­lab­o­ra­tive pro­to­type of an Open Agency Architecture

Deger TuranMay 10, 2023, 5:41 PM
31 points
0 comments12 min readLW link

I bet $500 on AI win­ning the IMO gold medal by 2026

azsantoskMay 11, 2023, 2:46 PM
37 points
29 comments1 min readLW link

Fun­da­men­tals of For­mal­i­sa­tion Level 5: For­mal Proof

philip_bJul 9, 2018, 8:55 PM
13 points
0 comments1 min readLW link

In­fra-Do­main proofs 1

DiffractorMar 28, 2021, 9:16 AM
13 points
0 comments23 min readLW link

In­fra-Do­main Proofs 2

DiffractorMar 28, 2021, 9:15 AM
13 points
0 comments21 min readLW link

Allow­ing a for­mal proof sys­tem to self im­prove while avoid­ing Lo­bian ob­sta­cles.

Donald HobsonJan 23, 2019, 11:04 PM
6 points
4 comments2 min readLW link

[Math] Towards Proof Writ­ing as a Skill In Itself

Andrew QuinnJun 13, 2018, 4:39 AM
25 points
8 comments2 min readLW link

The value of learn­ing math­e­mat­i­cal proof

JonahSJun 2, 2015, 3:15 AM
8 points
42 comments1 min readLW link

An Illus­trated Proof of the No Free Lunch Theorem

lifelonglearnerJun 8, 2020, 1:54 AM
19 points
0 comments1 min readLW link
(mlu.red)

An ex­am­ple of self-fulfilling spu­ri­ous proofs in UDT

cousin_itMar 25, 2012, 11:47 AM
33 points
43 comments2 min readLW link

Weak HCH ac­cesses EXP

evhubJul 22, 2020, 10:36 PM
16 points
0 comments3 min readLW link

Align­ment pro­pos­als and com­plex­ity classes

evhubJul 16, 2020, 12:27 AM
40 points
26 comments13 min readLW link

LBIT Proofs 5: Propo­si­tions 29-38

DiffractorDec 16, 2020, 3:35 AM
8 points
0 comments21 min readLW link

LBIT Proofs 1: Propo­si­tions 1-9

DiffractorDec 16, 2020, 3:48 AM
7 points
0 comments25 min readLW link

LBIT Proofs 6: Propo­si­tions 39-47

DiffractorDec 16, 2020, 3:33 AM
7 points
0 comments23 min readLW link

LBIT Proofs 2: Propo­si­tions 10-18

DiffractorDec 16, 2020, 3:45 AM
7 points
0 comments20 min readLW link

Proofs Sec­tion 2.3 (Up­dates, De­ci­sion The­ory)

DiffractorAug 27, 2020, 7:49 AM
8 points
0 comments31 min readLW link

Proofs Sec­tion 2.2 (Iso­mor­phism to Ex­pec­ta­tions)

DiffractorAug 27, 2020, 7:52 AM
8 points
0 comments46 min readLW link

A proof of Löb’s the­o­rem in Haskell

cousin_itSep 19, 2014, 1:01 PM
52 points
8 comments3 min readLW link

Coun­ter­fac­tual In­duc­tion (Al­gorithm Sketch, Fix­point proof)

DiffractorDec 17, 2019, 5:04 AM
5 points
2 comments7 min readLW link

Log­i­cal in­duc­tor limits are dense un­der poin­t­wise convergence

SamEisenstatOct 6, 2016, 8:07 AM
5 points
0 comments6 min readLW link

For­mal­ized math: dream vs reality

cousin_itJul 9, 2009, 8:51 PM
19 points
10 comments2 min readLW link

Progress on au­to­mated math­e­mat­i­cal the­o­rem prov­ing?

JonahSJul 3, 2013, 6:40 PM
26 points
65 comments1 min readLW link

Proofs Sec­tion 1.1 (Ini­tial re­sults to LF-du­al­ity)

DiffractorAug 27, 2020, 7:59 AM
8 points
0 comments20 min readLW link

Proofs Sec­tion 1.2 (Mix­tures, Up­dates, Push­for­wards)

DiffractorAug 27, 2020, 7:57 AM
8 points
0 comments14 min readLW link

Proofs Sec­tion 2.1 (The­o­rem 1, Lem­mas)

DiffractorAug 27, 2020, 7:54 AM
8 points
0 comments36 min readLW link

LBIT Proofs 4: Propo­si­tions 22-28

DiffractorDec 16, 2020, 3:38 AM
7 points
0 comments17 min readLW link

LBIT Proofs 7: Propo­si­tions 48-52

DiffractorDec 16, 2020, 3:31 AM
7 points
0 comments20 min readLW link

LBIT Proofs 8: Propo­si­tions 53-58

DiffractorDec 16, 2020, 3:29 AM
7 points
0 comments18 min readLW link

LBIT Proofs 3: Propo­si­tions 19-22

DiffractorDec 16, 2020, 3:40 AM
8 points
0 comments17 min readLW link

So­cial Choice The­ory and Log­i­cal Handshakes

StrivingForLegibilityDec 29, 2023, 3:49 AM
17 points
0 comments4 min readLW link

In­ter­view Daniel Mur­fet on Univer­sal Phenom­ena in Learn­ing Machines

Alexander Gietelink OldenzielFeb 6, 2023, 12:00 AM
50 points
1 comment16 min readLW link

Speedrun­ning 4 mis­takes you make when your al­ign­ment strat­egy is based on for­mal proof

QuinnFeb 16, 2023, 1:13 AM
63 points
18 comments2 min readLW link

Ques­tion/​Is­sue with the 5/​10 Problem

acgtNov 29, 2021, 10:45 AM
6 points
3 comments3 min readLW link

Plan­ning to build a cryp­to­graphic box with perfect secrecy

Lysandre TerrisseDec 31, 2023, 9:31 AM
40 points
6 comments11 min readLW link

Limi­ta­tions on For­mal Ver­ifi­ca­tion for AI Safety

Andrew DicksonAug 19, 2024, 11:03 PM
134 points
60 comments23 min readLW link

Towards Guaran­teed Safe AI: A Frame­work for En­sur­ing Ro­bust and Reli­able AI Systems

Joar SkalseMay 17, 2024, 7:13 PM
67 points
10 comments2 min readLW link

A list of core AI safety prob­lems and how I hope to solve them

davidadAug 26, 2023, 3:12 PM
165 points
29 comments5 min readLW link

An Opinionated Look at In­fer­ence Rules

Gianluca CalcagniSep 3, 2024, 1:32 PM
−5 points
2 comments13 min readLW link

Mea­sur­ing Non­lin­ear Fea­ture In­ter­ac­tions in Sparse Cross­coders [Pro­ject Pro­posal]

Jan 6, 2025, 4:22 AM
19 points
0 comments12 min readLW link

Video In­tro to Guaran­teed Safe AI

Jul 11, 2024, 5:53 PM
27 points
0 comments1 min readLW link
(youtu.be)

[Question] Search­ing for Im­pos­si­bil­ity Re­sults or No-Go The­o­rems for prov­able safety.

MaelstromSep 27, 2024, 8:12 PM
2 points
1 comment1 min readLW link

The Fun­da­men­tal Cir­cu­lar­ity The­o­rem: Why Some Math­e­mat­i­cal Be­havi­ours Are In­her­ently Unprovable

Alister MundayJan 22, 2025, 6:20 PM
−11 points
2 comments4 min readLW link
No comments.