Merge pull request #10 from bernborgess/Documentation

Documentation with Lean Snippets

.gitignore

@@ -1,8 +1,315 @@
+# Ignore book files, except for Lean's highlight.js
 /book
 
 /build
 /lakefile.olean
 /lake-packages/*
 
 /.vscode
-/.lake
+/.lake
+## Core latex/pdflatex auxiliary files:
+*.aux
+*.lof
+*.log
+*.lot
+*.fls
+*.out
+*.toc
+*.fmt
+*.fot
+*.cb
+*.cb2
+.*.lb
+
+## Intermediate documents:
+*.dvi
+*.xdv
+*-converted-to.*
+# these rules might exclude image files for figures etc.
+# *.ps
+# *.eps
+# *.pdf
+
+## Generated if empty string is given at "Please type another file name for output:"
+.pdf
+
+## Bibliography auxiliary files (bibtex/biblatex/biber):
+*.bbl
+*.bcf
+*.blg
+*-blx.aux
+*-blx.bib
+*.run.xml
+
+## Build tool auxiliary files:
+*.fdb_latexmk
+*.synctex
+*.synctex(busy)
+*.synctex.gz
+*.synctex.gz(busy)
+*.pdfsync
+*.rubbercache
+rubber.cache
+
+## Build tool directories for auxiliary files
+# latexrun
+latex.out/
+
+## Auxiliary and intermediate files from other packages:
+# algorithms
+*.alg
+*.loa
+
+# achemso
+acs-*.bib
+
+# amsthm
+*.thm
+
+# beamer
+*.nav
+*.pre
+*.snm
+*.vrb
+
+# changes
+*.soc
+
+# comment
+*.cut
+
+# cprotect
+*.cpt
+
+# elsarticle (documentclass of Elsevier journals)
+*.spl
+
+# endnotes
+*.ent
+
+# fixme
+*.lox
+
+# feynmf/feynmp
+*.mf
+*.mp
+*.t[1-9]
+*.t[1-9][0-9]
+*.tfm
+
+#(r)(e)ledmac/(r)(e)ledpar
+*.end
+*.?end
+*.[1-9]
+*.[1-9][0-9]
+*.[1-9][0-9][0-9]
+*.[1-9]R
+*.[1-9][0-9]R
+*.[1-9][0-9][0-9]R
+*.eledsec[1-9]
+*.eledsec[1-9]R
+*.eledsec[1-9][0-9]
+*.eledsec[1-9][0-9]R
+*.eledsec[1-9][0-9][0-9]
+*.eledsec[1-9][0-9][0-9]R
+
+# glossaries
+*.acn
+*.acr
+*.glg
+*.glo
+*.gls
+*.glsdefs
+*.lzo
+*.lzs
+*.slg
+*.slo
+*.sls
+
+# uncomment this for glossaries-extra (will ignore makeindex's style files!)
+# *.ist
+
+# gnuplot
+*.gnuplot
+*.table
+
+# gnuplottex
+*-gnuplottex-*
+
+# gregoriotex
+*.gaux
+*.glog
+*.gtex
+
+# htlatex
+*.4ct
+*.4tc
+*.idv
+*.lg
+*.trc
+*.xref
+
+# hypdoc
+*.hd
+
+# hyperref
+*.brf
+
+# knitr
+*-concordance.tex
+# TODO Uncomment the next line if you use knitr and want to ignore its generated tikz files
+# *.tikz
+*-tikzDictionary
+
+# listings
+*.lol
+
+# luatexja-ruby
+*.ltjruby
+
+# makeidx
+*.idx
+*.ilg
+*.ind
+
+# minitoc
+*.maf
+*.mlf
+*.mlt
+*.mtc[0-9]*
+*.slf[0-9]*
+*.slt[0-9]*
+*.stc[0-9]*
+
+# minted
+_minted*
+*.pyg
+
+# morewrites
+*.mw
+
+# newpax
+*.newpax
+
+# nomencl
+*.nlg
+*.nlo
+*.nls
+
+# pax
+*.pax
+
+# pdfpcnotes
+*.pdfpc
+
+# sagetex
+*.sagetex.sage
+*.sagetex.py
+*.sagetex.scmd
+
+# scrwfile
+*.wrt
+
+# svg
+svg-inkscape/
+
+# sympy
+*.sout
+*.sympy
+sympy-plots-for-*.tex/
+
+# pdfcomment
+*.upa
+*.upb
+
+# pythontex
+*.pytxcode
+pythontex-files-*/
+
+# tcolorbox
+*.listing
+
+# thmtools
+*.loe
+
+# TikZ & PGF
+*.dpth
+*.md5
+*.auxlock
+
+# titletoc
+*.ptc
+
+# todonotes
+*.tdo
+
+# vhistory
+*.hst
+*.ver
+
+# easy-todo
+*.lod
+
+# xcolor
+*.xcp
+
+# xmpincl
+*.xmpi
+
+# xindy
+*.xdy
+
+# xypic precompiled matrices and outlines
+*.xyc
+*.xyd
+
+# endfloat
+*.ttt
+*.fff
+
+# Latexian
+TSWLatexianTemp*
+
+## Editors:
+# WinEdt
+*.bak
+*.sav
+
+# Texpad
+.texpadtmp
+
+# LyX
+*.lyx~
+
+# Kile
+*.backup
+
+# gummi
+.*.swp
+
+# KBibTeX
+*~[0-9]*
+
+# TeXnicCenter
+*.tps
+
+# auto folder when using emacs and auctex
+./auto/*
+*.el
+
+# expex forward references with \gathertags
+*-tags.tex
+
+# standalone packages
+*.sta
+
+# Makeindex log files
+*.lpz
+
+# xwatermark package
+*.xwm
+
+# REVTeX puts footnotes in the bibliography by default, unless the nofootinbib
+# option is specified. Footnotes are the stored in a file with suffix Notes.bib.
+# Uncomment the next line to have this generated file ignored.
+#*Notes.bib

docs/introduction.md

@@ -4,20 +4,20 @@ Introduction
 Cutting Planes and Lean 4
 -----------------------------
 
-*Cutting Planes* is a formal logic used in the context of discrete combinatorial problems, that can be applied in _Software testing_, _Formal verification_ and _Proof logging_.
+*Cutting Planes* is a method in mathematical optimizaiton used in the context of discrete combinatorial problems, that can be applied in _Software testing_, _Formal verification_ and _Proof logging_.
+Pseudo-Boolean in the other hand is a logic system introduced by Jakob Nordström in his paper [A Unified Proof System for Discrete Combinatorial Problems](https://jakobnordstrom.se/docs/presentations/TalkVeriPB_Dagstuhl23.pdf#page=45), which this project aims to implement and verify.
+Our proofs will consist of _Pseudo-Boolean Constraints_, that are 0-1 integer linear inequalities. Without loss of generality, we will use the [normalized form](https://pure.mpg.de/rest/items/item_1832217_4/component/file_2574300/content#page=7).
 
-Our proofs will consist of _Pseudo-Boolean Constraints_, that are 0-1 integer linear inequalities of the form:
 \\[ \sum_i{a_i l_i} \ge A \\]
 Where we have:
-- constant \\( A \in \mathbb{Z} \\)
-- coefficients \\( a_i \in \mathbb{Z} \\)
+- constant \\( A \in \mathbb{N} \\)
+- coefficients \\( a_i \in \mathbb{N} \\)
 - literals \\( l_i: x_i\ \text{or}\ \overline{x_i}\ (\text{where } x_i + \overline{x_i} = 1) \\)
 - variables \\( x_i \\) take values \\( 0 = false \\) or \\( 1 = true \\)
 
-Without loss of generality, we will use the [normalized form](https://pure.mpg.de/rest/items/item_1832217_4/component/file_2574300/content#page=7), with all \\( a_i, A\\) non-negative.
 
 In this regard, _Pseudo-Boolean Reasoning_ works on two axioms and four rules, each of which are formally verified in this project using _Lean 4_
 
-[Lean 4](https://lean-lang.org/) is a theorem prover and programming language developed by [Leonardo de Moura](http://leodemoura.github.io/). In the last years it became proeminent in the mathematics community, after [The Xena Project](https://www.ma.imperial.ac.uk/~buzzard/xena/) of Imperial College London formalized Peter Scholze's proof in the area of condensed mathematics in 2021. In 2023 Terence Tao used Lean to formalize a proof of the _Polynomial Freiman-Ruzsa [(PFR)](https://teorth.github.io/pfr/) conjecture_, published in the same year.
+[Lean 4](https://lean-lang.org/) is a theorem prover and programming language developed by [Leonardo de Moura](http://leodemoura.github.io/). In the last years it became proeminent in the mathematics community, after Kevin Buzzard's [The Xena Project](https://www.ma.imperial.ac.uk/~buzzard/xena/) of Imperial College London was formed, aiming to formalize all undergraduate level math, Peter Scholze's proof in the area of condensed mathematics called [_Liquid Tensor Experiment_](https://github.com/leanprover-community/lean-liquid) was formalized in 2021 and in 2023 Terence Tao used Lean to formalize a proof of the _Polynomial Freiman-Ruzsa [(PFR)](https://teorth.github.io/pfr/) conjecture_, published in the same year.
 
 Armed with a Lean 4 proof of the reasoning rules, complex proofs that involve these steps can be guaranteed to be correct.

docs/poc.tex

@@ -0,0 +1,48 @@
+\documentclass[a4paper]{article}
+\usepackage{listings}
+\usepackage{color}
+
+% \lstset{style=bw}
+
+\begin{document}
+
+\section{Introduction}
+
+\[
+    \sum_i{a} = b + c
+\]
+
+%Custom Colors
+\definecolor{plainText}{RGB}{74,131,31}
+\definecolor{comments}{RGB}{74,131,31}
+\definecolor{strings}{RGB}{180,54,34}
+\definecolor{numbers}{RGB}{44,45,211}
+\definecolor{keywords}{RGB}{160,49,158}
+\definecolor{preprocessorStatements}{RGB}{109,75,48}
+\definecolor{classNames}{RGB}{101,63,165}
+
+
+\lstset{frame=tb,
+    language=C++,
+    aboveskip=3mm,
+    belowskip=3mm,
+    showstringspaces=false,
+    columns=flexible,
+    basicstyle={\small\ttfamily},
+    numbers=left,
+    numberstyle=\tiny\color{plainText},
+    keywordstyle=\color{keywords},
+    commentstyle=\color{comments},
+    stringstyle=\color{strings},
+    breaklines=true,
+    breakatwhitespace=true
+    tabsize=4
+}
+
+\lstset{language=python}
+\begin{lstlisting}
+    def foo:
+        print "oi"
+\end{lstlisting}
+
+\end{document}