# For­mal Proof

TagLast edit: 26 Sep 2021 22:04 UTC by

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

30 Oct 2012 13:02 UTC
126 points

# [talk] Os­bert Bas­tani—In­ter­pretable Ma­chine Learn­ing via Pro­gram Syn­the­sis—IPAM at UCLA

13 Jan 2023 1:38 UTC
9 points

# List of links: For­mal Meth­ods, Embed­ded Agency, 3d world mod­els, and some tools

23 Jan 2023 18:21 UTC
16 points

# A List of things I might do with a Proof Oracle

5 Feb 2023 18:14 UTC
−14 points

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

28 Aug 2019 10:46 UTC
4 points

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

17 Oct 2023 20:03 UTC
22 points
(blog.eleuther.ai)

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

8 Mar 2023 9:38 UTC
16 points

# In­fra-Do­main Proofs 2

28 Mar 2021 9:15 UTC
13 points

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

23 Jan 2019 23:04 UTC
6 points

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

13 Jun 2018 4:39 UTC
25 points

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

2 Jun 2015 3:15 UTC
7 points

# An Illus­trated Proof of the No Free Lunch Theorem

8 Jun 2020 1:54 UTC
19 points
(mlu.red)

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

25 Mar 2012 11:47 UTC
33 points

# Weak HCH ac­cesses EXP

22 Jul 2020 22:36 UTC
16 points

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

16 Jul 2020 0:27 UTC
40 points

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

16 Dec 2020 3:35 UTC
8 points

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

16 Dec 2020 3:48 UTC
7 points

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

16 Dec 2020 3:33 UTC
7 points

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

16 Dec 2020 3:45 UTC
7 points

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

27 Aug 2020 7:49 UTC
8 points

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

27 Aug 2020 7:52 UTC
8 points

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

19 Sep 2014 13:01 UTC
52 points

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

17 Dec 2019 5:04 UTC
5 points

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

29 Dec 2023 3:49 UTC
14 points

# For­mal­ized math: dream vs reality

9 Jul 2009 20:51 UTC
19 points

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

3 Jul 2013 18:40 UTC
26 points

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

27 Aug 2020 7:59 UTC
8 points

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

27 Aug 2020 7:57 UTC
8 points

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

27 Aug 2020 7:54 UTC
8 points

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

16 Dec 2020 3:38 UTC
7 points

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

16 Dec 2020 3:31 UTC
7 points

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

16 Dec 2020 3:29 UTC
7 points

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

16 Dec 2020 3:40 UTC
8 points

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

29 Nov 2021 10:45 UTC
6 points

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

6 Feb 2023 0:00 UTC
43 points

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

16 Feb 2023 1:13 UTC
62 points

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

6 Oct 2016 8:07 UTC
5 points

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

31 Dec 2023 9:31 UTC
37 points

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

19 Apr 2023 16:09 UTC
153 points

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

10 May 2023 17:41 UTC
30 points

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

11 May 2023 14:46 UTC
37 points