Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] cl-isabelle-users Digest Sat, 02 Aug 2025 (1/1)

view this post on Zulip Email Gateway (Aug 02 2025 at 04:05):

From: Saburou Saitoh <saburou.saitoh@gmail.com>
Dear the members:

Please look at the following paper for

many logical problems and great impacts of AI:

(DOI: 10.13140/RG.2.2.19833.17761

Division by Zero Calculus, Direction of Zero Vector and Fundamental

Equations of Vectors (Meanings of Zero)

Presentation

Filename: indsaitoh20250520.pdf)

Saburou Saitoh

2025.8.2.13:00

2025年8月2日(土) 12:01 <cl-isabelle-users-request@lists.cam.ac.uk>:

cl-isabelle-users digest Sat, 02 Aug 2025

Table of contents:

Message-ID: <6318090C-6840-41E6-9B2C-2A9674D87585@cam.ac.uk>
Date: Fri, 1 Aug 2025 10:57:35 +0000
From: Lawrence Paulson <lp15@cam.ac.uk>
Subject: [isabelle] New in the AFP: Unconstrained Optimization

I am happy to announce a new entry, Unconstrained Optimization, by Dustin
Bryant.

As formal methods gain traction in machine learning and numerical
analysis,
the community needs computer-checked proofs of core optimization results.
Existing Isabelle libraries still lack a foundational framework for
unconstrained optimization. We close this gap with a comprehensive
Isabelle/
HOL development that formalizes:
• minimizers, strict and isolated local minimizers;
• first- and second-order optimality conditions for scalar real-valued
functions;
• first-order optimality conditions for vector-valued functions; and
• a worked example.
The new session provides sound, reusable foundations for future proof-
checking tools and mechanized research in optimization, analysis, and
algorithmic correctness.

https://www.isa-afp.org/entries/Unconstrained_Optimization.html

Larry Paulson

Message-ID: <b998997e-1d87-45f9-a6d9-808d73504cab@Spark>
Date: Fri, 1 Aug 2025 14:57:08 +0000
From: Lawrence Paulson <lp15@cam.ac.uk>
Subject: [isabelle] Another little AI experiment

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!

End of cl-isabelle-users Digest Sat, 02 Aug 2025

Last updated: Aug 20 2025 at 20:23 UTC