Skip to content

fix typos on README.md #314

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
johnchandlerburnham merged 1 commit into from
Feb 25, 2026
Merged

fix typos on README.md #314

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ Our expectation is that Ix, and **zkPCC** in general, will allow applications to
security guarantees to their users. Some possible use cases could be:

- Software written in compiled languages like Rust can attach to their binaries
proofs of type signatures or other formal properties verified by tools
proofs of type signatures or other formal properties verified by tools such as
[Aeneas](https://github.com/AeneasVerif/aeneas). Given mature
certified compilation infrastructure (e.g. a future
[CompCert](https://en.wikipedia.org/wiki/CompCert) equivalent in Lean4),
Expand Down Expand Up @@ -93,7 +93,7 @@ Fermat's claim that he possessed a proof of the first part is credible, which
seems unlikely given the complexity and modern mathematical infrastructure used
by the Wiles proof of the first part. Rarely discussed, however, is the third
part, which is in fact a statement of proof theory, specifically one which
proposes a information theoretic lower bound to the size of the proof of a
proposes an information theoretic lower bound to the size of the proof of a
particular proposition.

The specific margin in question is [page 85 in the 1621 edition of Diophantus'
Expand All @@ -115,11 +115,11 @@ At 262 characters, and 8-bits per character, this is 2096 bits, or 262 bytes.
This is quite small, but fortunately not quite as small as a [Groth16 proof over
BN254](https://2π.com/23/bn254-compression/):

> A Groth16 proof has two G1 points and one G2. In the BN254 pairing curve these take 64 and 128 bytes respectively uncrompressed totaling 256 bytes for a proof.
> A Groth16 proof has two G1 points and one G2. In the BN254 pairing curve these take 64 and 128 bytes respectively uncompressed totaling 256 bytes for a proof.

So if we can show that a Groth16 proof of *a* proof of the first part of
Fermat's Last Theorem is constructible, we will have clearly - though
non-constructively- disproven the third part.
non-constructively- disproven the third part.

[A Lean 4 formalization of Fermat's Last
Theorem](https://github.com/ImperialCollegeLondon/FLT) is in progress, and gives
Expand Down