Merge requests · AVA / Dandelion

proved soundness of polynomial approximation of sqrt. changed the lemma...

!25 · created Jan 25, 2022 by Mohit Tekriwal
- Merged
- Approved
- 1
- 7
updated Jan 28, 2022
Add approximation of ln on the interval from 1 to infinity.

!24 · created Jan 21, 2022 by Heiko Becker
- Merged
- Approved
- 0
updated Jan 24, 2022
Tan mclaurin

!23 · created Nov 25, 2021 by Mohit Tekriwal
- Merged
- Approved
- 1
- 1
updated Nov 26, 2021
Merge current state of atan/ tan branch to use them for approximating pi

!22 · created Nov 11, 2021 by Heiko Becker
- Merged
- Approved
- 0
updated Nov 11, 2021
Proved the mclaurin series lemma for sqrt(1+x).

!21 · created Sep 20, 2021 by Mohit Tekriwal master
- Merged
- Approved
- 18
updated Sep 27, 2021
Proved the mclaurin series lemma for sqrt(1+x).

!20 · created Sep 19, 2021 by Mohit Tekriwal master
- Closed
- 0
updated Sep 19, 2021
Mclaurin series and first checker implementation with soundness

!19 · created Aug 30, 2021 by Heiko Becker master
- Merged
- Approved
- 0
updated Aug 30, 2021
Modified the definition of validateZeroesLeqErr_def and prove its soundness

!18 · created Aug 26, 2021 by Heiko Becker master
- Merged
- Approved
- 0
updated Aug 26, 2021
Copied the proof of the lemma REAL_EXP_BOUND_LEMMA from HOL light.

!17 · created Aug 24, 2021 by Heiko Becker master
- Merged
- Approved
- 0
updated Aug 24, 2021
Fixed issues in the definitions in the realPolyScript file and proved...

!16 · created Aug 23, 2021 by Mohit Tekriwal master
- Merged
- Approved
- 1
- 1
updated Aug 24, 2021
Add a mock-up certificate checker

!15 · created Aug 13, 2021 by Heiko Becker master
- Merged
- 4
updated Aug 18, 2021
Add a computable version of sturm sequences

!14 · created Aug 13, 2021 by Heiko Becker master
- Merged
- Approved
- 2
updated Aug 13, 2021
sollya example

!13 · created Aug 10, 2021 by Mohit Tekriwal master
- Merged
- Approved
- 1
- 1
updated Aug 10, 2021
Sollya example by Anastasia

!12 · created Aug 09, 2021 by Mohit Tekriwal master
- Closed
- 1
updated Aug 10, 2021
Port more proofs of John Harrisons original paper

!11 · created Jul 12, 2021 by Heiko Becker master
- Merged
- 0
updated Jul 12, 2021
Port upper bound lemmas from John Harrisons material to HOL4

!10 · created Jul 12, 2021 by Heiko Becker master
- Closed
- Approved
- 0
updated Jul 12, 2021
Add a mock-up example generated from Sollya and input file

!9 · created Jul 12, 2021 by Heiko Becker master
- Merged
- Approved
- 4
updated Jul 12, 2021
Sollya sturm document

!8 · created Jul 08, 2021 by Mohit Tekriwal master
- Merged
- Approved
- 1
- 9
updated Jul 09, 2021
Replace sturmScript.sml with the fixed version

!7 · created Jul 08, 2021 by Mohit Tekriwal master
- Merged
- Approved
- 1
- 1
updated Jul 08, 2021
Porting theorems from HOL light to HOL4

!6 · created Jul 05, 2021 by Mohit Tekriwal master
- Merged
- Approved
- 1
- 5
updated Jul 08, 2021