\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{proof}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations}

[[!include foundations - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{Proof}{In type theory}\dotfill \pageref*{Proof} \linebreak
\noindent\hyperlink{FormalProof}{Formal proofs}\dotfill \pageref*{FormalProof} \linebreak
\noindent\hyperlink{RelationToObservationInPhysics}{Relation to observation in physics}\dotfill \pageref*{RelationToObservationInPhysics} \linebreak
\noindent\hyperlink{ProofMethods}{Proof methods}\dotfill \pageref*{ProofMethods} \linebreak
\noindent\hyperlink{LibrariesOfFormalProofs}{Libraries of formal proofs}\dotfill \pageref*{LibrariesOfFormalProofs} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

\begin{quote}%
The interesting conception of the [[propositions-as-types]] principle is what I call \emph{Brouwer's Dictum}, which states that all of mathematics, including the concept of a proof, is to be derived from the concept of a \emph{[[constructive mathematics|construction]]}, a [[computation]] classified by a [[type]]. In [[intuitionistic mathematics]] proofs are themselves ``first-class'' mathematical objects that inhabit [[type|types]] that may as well be identified with the [[proposition]] that they prove. Proving a proposition is no different than constructing a [[program]] of a type. In this sense [[logic]] is a branch of [[mathematics]], the branch concerned with those constructions that are proofs. And mathematics is itself a branch of [[computer science]], since according to Brouwer's Dictum all of mathematics is to be based on the concept of computation. But notice as well that there are many more constructions than those that correspond to proofs. [[natural number|Numbers]], for example, are perhaps the most basic ones, as would be any [[inductive type|inductive]] or [[coinductive type|coinductive]] types, or even more exotic objects such as Brouwer's own [[choice sequence]]s. From this point of view the [[judgement]] $t\in A$ stating that $t$ is a [[term|construction]] of type $A$ is of fundamental importance, since it encompasses not only the formation of ``ordinary'' mathematical constructions, but also those that are distinctively intuitionistic, namely mathematical proofs.

An often misunderstood point that must be clarified before we continue is that the concept of proof in [[intuitionistic logic|intuitionism]] is \emph{not} to be identified with the concept of a \emph{formal proof} in a fixed formal system. What constitutes a proof of a [[proposition]] is a \emph{[[judgement]]}, and there is no reason to suppose \emph{a priori} that this judgement ought to be [[decidable judgment|decidable]]. It should be possible to recognize a proof when we see one, but it is not required that we be able to \emph{rule out} what is a proof in all cases. In contrast formal proofs are inductively defined and hence fully circumscribed, and we expect it to be decidable whether or not a purported formal proof is in fact a formal proof, that is whether it is well-formed according to the given inductively defined rules. But the upshot of [[incompleteness theorem|Gödel's theorem]] is that as soon as we fix the concept of formal proof, it is immediate that it is not an adequate conception of proof \emph{simpliciter}, because there are propositions that are true, which is to say have a proof, but have no \emph{formal proof} according to the given rules. The concept of truth, even in the intuitionistic setting, eludes formalization, and it will ever be thus. Putting all this another way, according to the intuitionistic viewpoint (and the mathematical practices that it codifies), there is no truth other than that given by proof. Yet the rules of proof cannot be given in decidable form without missing the point. (\hyperlink{Harper}{Harper})


\end{quote}
\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

\begin{itemize}%
\item \hyperlink{Proof}{In type theory}


\item \hyperlink{FormalProof}{Formal proofs}



\end{itemize}
\hypertarget{Proof}{}\subsubsection*{{In type theory}}\label{Proof}

In [[type theory]], a [[proposition]] is identified with the [[type]] of all its proofs (the \emph{[[propositions as types]]}-aspect of [[computational trinitarianism]]). Here a proof consists of exhibiting a [[term]] of the corresponding type (showing that it is [[inhabited]]), hence a proof is a typing [[judgement]] for a term of the type representing the proposition.

See also \emph{[[proofs as programs]]}.

\hypertarget{FormalProof}{}\subsubsection*{{Formal proofs}}\label{FormalProof}

A [[formal proof]] is whatever is called a `proof' in a formal system; a formal system for [[mathematics]] then gives rules for producing a proof in the above sense. Typically, a formal system is [[induction|inductively]] defined, and hence its proofs are fully circumscribed; this is the case for [[deductive systems]] such as [[natural deduction]], [[sequent calculus]], and [[Hilbert systems]]. [[incompleteness theorem|Gödel's theorem]] suggests, however, that no such system can encapsulate all of mathematics.

\hypertarget{RelationToObservationInPhysics}{}\subsection*{{Relation to observation in physics}}\label{RelationToObservationInPhysics}

In (\href{JaffeQuinn93}{Jaffe-Quinn 93, p. 2}) it was claimed that

\begin{quote}%
 the role of rigorous [[proof]] in mathematics is functionally [[analogy|analogous]] to the role of [[experiment]] in the natural sciences


\end{quote}
\begin{uremark}
After making this statement about proof as observation, the article by Jaffe-Quinn goes further to suggest that the analogue in physics of speculation and conjecture in mathematics is the realm of theoretical physics, and then maybe even further in suggesting that mathematics could reasonably be purely ``theoretical'' in this sense. These further claims were considered faulty by several authors (\href{http://arxiv.org/abs/math/9404229}{math/9404229}).

([[Saunders MacLane]] in particular argued for theorems and proofs as the final goal of a piece of developed mathematics, and emphasized the explanatory function of proofs. This in contrast with experiment in physics, which is neither considered as the final goal nor as playing an explanatory role.)

While all this does contradict some of Jaffe-Quinn's claims, it may still harmonize with the statement \hyperlink{JaffeQuinnProofIsObservation}{above}. Indeed, another perspective on the claim is that finding a proof is an observational or witnessing act, which resonates with the nature of proof in [[constructive mathematics]], such as made manifest in the [[propositions as types]]-paradigm. This perspective sees proof as something more than merely establishing the truth of a proposition.

\begin{quote}%
\ldots{} to show that a proposition is true in type theory corresponds to exhibiting an element $[$ [[term]] $]$ of the type corresponding to that proposition. We regard the elements of this type as \emph{evidence} or \emph{witnesses} that the proposition is true. (They are sometimes even called \emph{proofs}\ldots{} (from [[Homotopy Type Theory -- Univalent Foundations of Mathematics]], section 1.11)


\end{quote}
Thus a proof \emph{qua} witness is a construction, and in more elaborated developments (for instance in [[intensional type theory]]) a formal proof is itself a mathematical object, with internal mathematical structure.

\end{uremark}
\hypertarget{ProofMethods}{}\subsection*{{Proof methods}}\label{ProofMethods}

\begin{itemize}%
\item [[refutation by contradiction]]


\item [[proof by contradiction]],



\end{itemize}
\hypertarget{LibrariesOfFormalProofs}{}\subsection*{{Libraries of formal proofs}}\label{LibrariesOfFormalProofs}

Libraries of [[formal proofs]] formalized in some [[proof assistant]]:

\begin{itemize}%
\item [[UniMath project]]


\item [[Xena project]]


\item [[ForMath project]]


\item [[Archive of Formal Proofs]]


\item [[The QED Project]]



\end{itemize}
\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[computational trinitarianism]]


\item [[theory]]


\item [[proposition]]/[[type]] ([[propositions as types]])


\item [[definition]]/\textbf{proof}/[[program]] ([[proofs as programs]])


\item [[theorem]], [[axiom]]


\item [[proof theory]]



\end{itemize}
[[!include proof assistants and formalization projects -- list]]

\hypertarget{references}{}\subsection*{{References}}\label{references}

A brief exposition of the notion of proof and formal proof in [[constructive mathematics]]/[[type theory]] is in

\begin{itemize}%
\item [[Robert Harper]], \emph{Extensionality, Intensionality, and Brouwer's Dictum}, August 2012 (\href{http://existentialtype.wordpress.com/2012/08/11/extensionality-intensionality-and-brouwers-dictum/}{web})


\item [[Robert Harper]], \emph{Constructive Mathematics is not Meta-Mathematics}, July 2013 (\href{http://existentialtype.wordpress.com/2013/07/10/constructive-mathematics-is-not-meta-mathematics/}{web})



\end{itemize}
Further discussion of formal proofs includes the following

\begin{itemize}%
\item [[Thomas Hales]], \emph{Formal proof} (\href{http://www.ams.org/notices/200811/tx081101370p.pdf}{pdf})


\item John Harrison, \emph{Formal proof -- theory and practice} (\href{http://www.ams.org/notices/200811/tx081101395p.pdf}{pdf})


\item [[Jeremy Avigad]], Kevin Donnelly, David Gray, Paul Raff, \emph{A formally verified proof of the prime number theorem} (\href{http://arxiv.org/abs/cs/0509025}{arXiv:cs/0509025})


\item [[Jeremy Avigad]], John Harrison, \emph{Formally Verified Mathematics}, Communications of the ACM, Vol. 57 No. 4, Pages 66-75 (\href{http://cacm.acm.org/magazines/2014/4/173219-formally-verified-mathematics/fulltext}{web})


\item [[Jeremy Avigad]], \emph{Formal verication, interactive theorem proving, and automated reasoning} (2014) (\href{http://www.andrew.cmu.edu/user/avigad/Talks/baltimore.pdf}{pdf})



\end{itemize}
A discussion of the relation of mathematical proof to [[phenomenology]] of [[theories]] of [[physics]] is in

\begin{itemize}%
\item [[Alexandre Miquel]], \emph{The experimental effectiveness of mathematical proof} (\href{http://perso.ens-lyon.fr/alexandre.miquel/publis/effectiveness.pdf}{pdf})

\end{itemize}
Texts on genuine [[proof theory]] include

\begin{itemize}%
\item [[Richard Statman]], \emph{[[Structural Complexity of Proofs]]}, 1974

\end{itemize}
Projects aiming to formalize parts of mathematics include

\begin{itemize}%
\item [[ForMath]]


\item [[The QED Project]]


\item \href{https://xenaproject.wordpress.com/2018/10/07/what-is-the-xena-project/}{Xena} (by [[Kevin Buzzard]])



\end{itemize}
Consideration of the relation of mathematical proof to physics icludes

\begin{itemize}%
\item [[Arthur Jaffe]], [[Frank Quinn]], \emph{``Theoretical Mathematics'': Towards a cultural synthesis of mathematics and theoretical physics}, Bulletin of the AMS, Volume 29,Number 1, July 1993 (\href{http://arxiv.org/abs/math/9307227}{arXiv:math/9307227})

\end{itemize}
[[!redirects proof]] [[!redirects proofs]]

[[!redirects formal proof]] [[!redirects formal proofs]]



\end{document}