RSS

For­mal Proof

TagLast edit: 26 Sep 2021 22:04 UTC 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 Yudkowsky30 Oct 2012 13:02 UTC
126 points
218 comments12 min readLW link

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

the gears to ascension13 Jan 2023 1:38 UTC
9 points
1 comment1 min readLW link
(www.youtube.com)

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

the gears to ascension23 Jan 2023 18:21 UTC
16 points
1 comment17 min readLW link

A List of things I might do with a Proof Oracle

Logan Zoellner5 Feb 2023 18:14 UTC
−14 points
13 comments3 min readLW link

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

Davidmanheim28 Aug 2019 10:46 UTC
4 points
9 comments1 min readLW link

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

mako yass17 Oct 2023 20:03 UTC
22 points
0 comments1 min readLW link
(blog.eleuther.ai)

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

Donald Hobson8 Mar 2023 9:38 UTC
16 points
1 comment2 min readLW link

In­fra-Do­main Proofs 2

Diffractor28 Mar 2021 9:15 UTC
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 Hobson23 Jan 2019 23:04 UTC
6 points
4 comments2 min readLW link

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

Andrew Quinn13 Jun 2018 4:39 UTC
25 points
8 comments2 min readLW link

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

JonahS2 Jun 2015 3:15 UTC
7 points
42 comments1 min readLW link

An Illus­trated Proof of the No Free Lunch Theorem

lifelonglearner8 Jun 2020 1:54 UTC
19 points
0 comments1 min readLW link
(mlu.red)

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

cousin_it25 Mar 2012 11:47 UTC
33 points
43 comments2 min readLW link

Weak HCH ac­cesses EXP

evhub22 Jul 2020 22:36 UTC
16 points
0 comments3 min readLW link

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

evhub16 Jul 2020 0:27 UTC
40 points
26 comments13 min readLW link

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

Diffractor16 Dec 2020 3:35 UTC
8 points
0 comments21 min readLW link

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

Diffractor16 Dec 2020 3:48 UTC
7 points
0 comments25 min readLW link

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

Diffractor16 Dec 2020 3:33 UTC
7 points
0 comments23 min readLW link

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

Diffractor16 Dec 2020 3:45 UTC
7 points
0 comments20 min readLW link

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

Diffractor27 Aug 2020 7:49 UTC
8 points
0 comments31 min readLW link

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

Diffractor27 Aug 2020 7:52 UTC
8 points
0 comments46 min readLW link

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

cousin_it19 Sep 2014 13:01 UTC
52 points
8 comments3 min readLW link

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

Diffractor17 Dec 2019 5:04 UTC
5 points
2 comments7 min readLW link

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

StrivingForLegibility29 Dec 2023 3:49 UTC
14 points
0 comments4 min readLW link

For­mal­ized math: dream vs reality

cousin_it9 Jul 2009 20:51 UTC
19 points
10 comments2 min readLW link

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

JonahS3 Jul 2013 18:40 UTC
26 points
65 comments1 min readLW link

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

Diffractor27 Aug 2020 7:59 UTC
8 points
0 comments20 min readLW link

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

Diffractor27 Aug 2020 7:57 UTC
8 points
0 comments14 min readLW link

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

Diffractor27 Aug 2020 7:54 UTC
8 points
0 comments36 min readLW link

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

Diffractor16 Dec 2020 3:38 UTC
7 points
0 comments17 min readLW link

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

Diffractor16 Dec 2020 3:31 UTC
7 points
0 comments20 min readLW link

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

Diffractor16 Dec 2020 3:29 UTC
7 points
0 comments18 min readLW link

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

Diffractor16 Dec 2020 3:40 UTC
8 points
0 comments17 min readLW link

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

acgt29 Nov 2021 10:45 UTC
6 points
3 comments3 min readLW link

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

Alexander Gietelink Oldenziel6 Feb 2023 0:00 UTC
43 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

Quinn16 Feb 2023 1:13 UTC
62 points
18 comments2 min readLW link

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

SamEisenstat6 Oct 2016 8:07 UTC
5 points
0 comments6 min readLW link

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

Lysandre Terrisse31 Dec 2023 9:31 UTC
37 points
6 comments11 min readLW link

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

19 Apr 2023 16:09 UTC
153 points
27 comments21 min readLW link

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

Deger Turan10 May 2023 17:41 UTC
30 points
0 comments12 min readLW link

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

azsantosk11 May 2023 14:46 UTC
37 points
27 comments1 min readLW link

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

philip_b9 Jul 2018 20:55 UTC
13 points
0 comments1 min readLW link

In­fra-Do­main proofs 1

Diffractor28 Mar 2021 9:16 UTC
13 points
0 comments23 min readLW link
No comments.