matematiflo/SumsOfSquares

Summing squares in Lean

Sums of squares

A Lean package that develops the basic theory of sums of squares in rings and fields. Our ultimate goal is to define a function that sends an ordered field to its real closure.

Libraries

• Definitions and examples
• Basic properties for lists
• The type of sums of squares
• Some exercises

Quickstart

Clone the repository

You can clone the repo using GitHub Desktop or via the command line

git clone https://github.com/matematiflo/SumsOfSquares.git

Alternately, just click on the Code button of the current repository.

If you have Lean 4

If you already have Lean 4 installed on your machine, just download the compiled Mathlib files via the command line

lake exe cache get

and then build the project by running the command line

lake build

If you do not have Lean 4

If you need to install Lean, you can go to the Lean Community portal and follow the instructions there, depending on your OS. Alternately, you can also look at the Lean Manual or at this repo.

After installing Lean, you will be able to run the command lines lake exe cache get and lake build indicated above.

Troubleshooting

If either lake exe cache get or lake build are not recongnized, try

curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain

and then

lake update

before trying lake exe cache get and lake build again.

Example file

You can run Example.lean either with the following command line

lake env lean Example.lean

Alternately, if you have already built the project (using lake build), you can simply execute the example binary file via

./build/bin/example

Codespaces

If you wish to work on this project online and without installing anything, you can do so by opening a Codespace. Just follow the link below and click on Create new codespace (GitHub account required).

Alternately, you can open a Codespace by clicking on the Code button of the current repository (possibly slower, though).

If you commit any modified file from within your Codespace, the repo will be forked to your GitHub account and your work will be saved there.

To leave a Codespace, it is recommended that you stop it before closing the browser window:

1. Click on your Codespace name at the bottom-left of the VS Code interface.
2. Choose Stop current Codespace from the list of options.
3. Wait until the Codespace has stopped to close your browser tab.

To access a Codespace that you have previously created, just go to

https://github.com/codespaces

or launch them directly from the Code button of the relevant repository (no setup required this time!).