Skip to content

Commit

Permalink
update abstract
Browse files Browse the repository at this point in the history
  • Loading branch information
pitmonticone committed Jun 12, 2024
1 parent e4d8ce5 commit aa26551
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
4 changes: 2 additions & 2 deletions blueprint/src/print.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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}

Expand All @@ -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})
Expand Down
2 changes: 1 addition & 1 deletion blueprint/src/web.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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})
Expand Down

0 comments on commit aa26551

Please sign in to comment.