[Afp-submit] AFP entry Neural_Networks

[Peter Lammich]

I remember having seen a talk about that ... but I cannot find any 
matching papers :(


On 20/11/2025 15:40, Lawrence Paulson wrote:
> I know that converting a floating point number to decimal notation is 
> tricky, but we must've had correct algorithms for decades now. I 
> wonder whether anybody has formalised one :-)
>
> Larry
> On 20 Nov 2025 at 13:21 +0000, Achim D. Brucker <adbrucker at 0x5f.org>, 
> wrote:
>>
>> This is also my assumption.  The values used by me in the below example
>> are after pretty printing (i.e., convertio to strings).
>>
>> The actually value stored is 0.070820772089064121246337890625 (decoding
>> it "manually", following the standard). Trying to print it in a small C
>> programm gives 0.00708207720890641212, which seems to be the offical
>> decimal represenation according to the standard. IEEE754  is not easy ...
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251120/baa4cd35/attachment.htm>