From 1eb20193a29b8657d454cbe4d1d793dfabb93373 Mon Sep 17 00:00:00 2001
From: Randall Holmes <rholmes@boisestate.edu>
Date: Wed, 4 Sep 2024 11:19:52 -0600
Subject: [PATCH] Update index.html

---
 index.html | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/index.html b/index.html
index eba3282..3035177 100644
--- a/index.html
+++ b/index.html
@@ -76,6 +76,9 @@ <h2>NF Consistency Proof</h2>
 I have claimed since 2010 to be in possession of a proof of the consistency of Quine's set theory New Foundations.<p>  
 
 <B>The formal verification of my proof of Con(NF) in Lean has been completed,</B> by Sky Wilshaw, a Part III student at Cambridge who is about to go on to her doctoral studies in Computer Science.<p>
+
+<A HREF="https://Randall-Holmes.github.io/Nfproof/maybedetangled2-for-arxiv.pdf">Here</A> is a newer version, reflecting collaboration of both authors, notably on improving the presentation of the Freedom of Action theorem.<p>
+
 <A HREF="https://Randall-Holmes.github.io/Nfproof/maybedetangled2.pdf">Here</A> is a version of the paper proof which is being edited to conform better with the approach that Sky took in the formalization.
 I have verified that the conclusions of the formal argument in Lean say the right thing:  it shows that there is a structure for the language of tangled type theory which satisfies all typed versions of statements in the finite axiomatization of NF due to Hailperin,
 which entails that it is in fact a model of tangled type theory, and so that New Foundations is consistent.  This version of the paper proof is still being edited to conform with the formalization,