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
112 points
218 comments12 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

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
17 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
14 points
0 comments3 min readLW link

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

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

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

Diffractor16 Dec 2020 3:35 UTC
7 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
7 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
7 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

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

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
25 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
6 points
0 comments20 min readLW link

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

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

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

Diffractor27 Aug 2020 7:54 UTC
7 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
7 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
No comments.