4 ms·
Building the Reasoning Engine at Axiom
- ux266478 1y ago> Mathematics needs something compilers never achieved: a true bidirectional cycle > Going down the stack: Autoformalization translates intuitive mathematical reasoning into formal proof – the compiler's traditional direction. > Going up the stack: Autoinformalization translates formal proofs back into human intuition – something compilers never truly do. We actually achieved this in the 1970s. It's called an expert system. They're very powerful tools and massively underutilized across all sectors. https://en.wikipedia.org/w/index.php?title=Mycin https://en.wikipedia.org/w/index.php?title=Mycin