diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex index 675e6f7..266cd83 100644 --- a/blueprint/src/print.tex +++ b/blueprint/src/print.tex @@ -33,7 +33,7 @@ \addbibresource{references.bib} % Set title and subtitle -\title{Formalising Fermat's Last Theorem for Exponent 3 in Lean} +\title{\textbf{Formalising Fermat's Last Theorem for Exponent 3 in Lean}} % Set date \date{\today} @@ -45,7 +45,7 @@ % Add the abstract \begin{abstract} This paper serves as the blueprint for the project aimed at formalising Fermat’s Last Theorem - for the exponent 3 (\href{https://github.com/pitmonticone/FLT3}{FLT3}) using the Lean 4 proof assistant. + for the exponent 3 using the Lean 4 proof assistant (\href{https://github.com/pitmonticone/FLT3}{FLT3}). It offers comprehensive coverage of all necessary definitions, theorems, and proofs, presented in natural, informal language to facilitate understanding and implementation. The related code is being integrated into the Lean library of formalized mathematics (\href{https://github.com/leanprover-community/mathlib4}{Mathlib}) diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex index d93b414..0d55e97 100644 --- a/blueprint/src/web.tex +++ b/blueprint/src/web.tex @@ -53,7 +53,7 @@ % Add the abstract \begin{abstract} This website serves as the blueprint for the project aimed at formalising Fermat’s Last Theorem - for the exponent 3 (\href{https://github.com/pitmonticone/FLT3}{FLT3}) using the Lean 4 proof assistant. + for the exponent 3 using the Lean 4 proof assistant (\href{https://github.com/pitmonticone/FLT3}{FLT3}). It offers comprehensive coverage of all necessary definitions, theorems, and proofs, presented in natural, informal language to facilitate understanding and implementation. The related code is being integrated into the Lean library of formalized mathematics (\href{https://github.com/leanprover-community/mathlib4}{Mathlib})