Email Gateway (Aug 01 2025 at 14:57): Email Gateway (Aug 01 2025 at 14:57):From: Lawrence Paulson <lp15@cam.ac.uk>
I asked ChatGPT the following question (about the sine integral function Si) and got quite a reasonable answer. Theory Sinc_Integral indeed exists in HOL-Probability and develops the function’s theory. To be sure, if you look carefully, you will note some anomalies. Still I think it is pretty good!
Larry
Is Si(x) or anything related formalised in Isabelle/HOL?
There is a formalization of the sine integral function
S i ( x ) in Isabelle/HOL, embedded within its measure‑theory and complex‑analysis libraries.
:check: Formalization in Isabelle/HOL
Isabelle/HOL includes a theory named Sinc_Integral (or similar), which defines and analyzes the sine integral function S i ( x ) . Among other results, it formally establishes:
* The definition of S i ( x ) = ∫ 0 x sin t t d t ,
* Its convergence as x → ∞ , proving that S i ( x ) → π 2 at infinity (cl.cam.ac.uk<https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL-Probability/Sinc_Integral.html?utm_source=chatgpt.com>, diofant.readthedocs.io<https://diofant.readthedocs.io/en/latest/modules/functions/special.html?utm_source=chatgpt.com>).
This is built on top of Isabelle's formal Lebesgue integration and Bochner integration framework.
:books: Broader Context
* Complex analysis of sine/cosine: Isabelle's Complex_Transcendental.thy (in HOL/Analysis) includes rigorous development of complex sine, cosine, exponential, Taylor series for trigonometric functions, and related transcendental lemmas (ResearchGate<https://www.researchgate.net/publication/221234907_On_the_Formalization_of_the_Lebesgue_Integration_Theory_in_HOL?utm_source=chatgpt.com>, isabelle.in.tum.de<https://isabelle.in.tum.de/repos/isabelle/diff/f03a01a18c6e/src/HOL/Analysis/Complex_Transcendental.thy?utm_source=chatgpt.com>).
* Integration theory: Isabelle’s libraries include comprehensive formalization of Lebesgue and interval integration, ported partially from HOL4 and expanded to support real and complex integrals, enabling the formal treatment of special integrals like Si (x) (ResearchGate<https://www.researchgate.net/publication/221234907_On_the_Formalization_of_the_Lebesgue_Integration_Theory_in_HOL?utm_source=chatgpt.com>).
:brain: So to sum up:
Item Formalized in Isabelle/HOL?
Definition of Si(x) :check: Yes (integral from 0 to x)
Convergence to π/2 :check: Yes
Related complex/trigonometric internals :check: Yes (series, sin, cos, exp)
:push_pin: If you're looking to work with Si (x) in Isabelle/HOL:
* Search for the Sinc_Integral theory in the Isabelle AFP or standard library (HOL-Probability or HOL/Analysis).
* You'll find definitions, lemmas like Si_at_top, and convergence proofs.
* You can then build on this to derive additional properties, asymptotic expansions, or differential identities.
:info: Additional note
There doesn’t seem to be a dedicated named theory like Si_Func, but in context of sinc integrals and Trigonometric integrals, it's covered thoroughly under measure-integral infrastructure.
Let me know if you'd like pointers to specific lemmas or examples of using Si(x) in Isabelle proofs!
Last updated: Aug 20 2025 at 20:23 UTC