_ouml_

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 helpful. But like the sibling comment says, AI is not the main point.

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 and (ii) automation of finding the proofs. The latter is very much an active field of research, but so far isn't of the level that it will prove most of your theorems for you.

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, flipflops etc...

I use the videos from Ben Eater as inspiration but I haven't told my daughter that you can build a programmable CPU using this stuff. I don't want to spoil the surprise.

After learning binary numbers, I asked her if she could build a circuit to add two digits. She designed her own version of a full adder, chained 4 of them together, and now has her own 4-bit calculator.

The cool thing is that she will explain it in detail to anybody who wants to listen. But she is also quickly discovering that modt people don't know binary...

What I like most about this is that she is now hacking independently, and having here own ideas. At some point I might teach her some formulas, but she hasn't shown interest there. And the occasional LED burning up isn't going to make me bankrupt (-;

Tl;dr: breadboard electronics is cool, worked with my 9yo daughter

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 answer.

@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://leanprover-community.github.io/mathlib_docs/measure_...

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 to automatically deduce that it is also a ring or a topological space, etc...)