_ouml_

3 ms·

1. 1.▲
   by _ouml_ 6y ago

   There is a very active community around Lean ranging from mathematicians with no clue about computers to AI researchers trying to improve the automation. These AI researchers have explicitly said that bigger training sets will be very helpf
2. 2.▲
   by _ouml_ 6y ago

   Yes, these systems are being used to formally verify implementations of cryptographic protocols, or implementations of numerical algorithms, for example. Note that there are two distinct components that interact: (i) verification of proofs
3. 3.▲
   by _ouml_ 6y ago

   Two months ago I bought a starter kit with some electronics: breadboards, LEDs, cables, transistors, resistors, etc... My 8/9yo daughter really got hooked, and since then I've bought all kinds of logic gates, switches, timers, fli
4. 4.▲
   by _ouml_ 6y ago

   The equality test is equivalent to deciding if something is 0. You can probably ask the app to calculate sqrt(2) * sqrt(2). If that doesn't show a 2 as answer, you've lost. Same goes for sin(arcsin(1/2)). You want the exact a
5. 5.▲
   by _ouml_ 6y ago

   @somethingsome If you want to turn arbitrary maths into code, you should take a look at interactive proof assistants. I'm a fan of https://leanprover-community.github.io/ It has Borel spaces: https://leanpro
6. 6.▲
   by _ouml_ 6y ago

   See page 4 of https://leanprover-community.github.io/papers/mathlib-paper.... for a part of the hierarchy of algebraic structures in the Lean theorem prover. (If you give it a normed field, it will use this hierarchy t