activity
20092023
most citedExploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar

20 citations · 86 across the 12 of their papers we have counts for

collaborators
Showing math.LOShow all

1 paper · 1 filter

math.LO2019

Cantor-Bernstein implies Excluded Middle

Cécilia Pradic, Chad E. Brown

We prove in constructive logic that the statement of the Cantor-Bernstein theorem implies excluded middle. This establishes that the Cantor-Bernstein theorem can only be proven ass…