# Re: [isabelle] G.U.T.

At TPHOLS 2009 Osman Hasan, Sanaz Khan Afshar and Sofiene Tahar
presented "Formal Analysis of Optical Waveguides in HOL" which is about
formalizing some physical properties in HOL4. As far as I know, physics
is mostly about calculus, so the Multivariate Analysis found in
HOL-light or Isabelle/HOL and the probability theory available in HOL4
and now also in Isabelle/HOL could be a good starting point.
Multivariate Analysis does also support non-euclidean spaces, which is
surely needed for the theory of relativity, and the probabilty theory
could be helpfully when formalizing quantum problems. So formalizing
some well established physics should be no problem. But how can
formalizing physics help when no theories are available for G.U.T.?
Greetings,
Johannes
Am Mittwoch, den 06.10.2010, 08:03 +0200 schrieb Jens Doll:
> Yesterday I heard that the string theory is out, because several aspects
> of it have been disproved. The task seems to lie in unifying the
> theories of relativity and quantum to a Grand United Theory. As
> physicists work mainly with mathematical modeling, I asked myself how
> these two theories could be united automatically by using an inference
> engine or something else (Isabelle?) and afterwards be tested if the result
> satisfies measured data.
>
> Where could I find a source for reasoning mathematically about physical
> phenomena? Does anyone here have a clue for it?
>
> Regards,
> Jens
>
> PS: GUT is a German word and means GOOD.
>
>

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*