> 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
ux266478•1h ago
> 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