We're excited to announce that AXLE is switching from Lean to Rocq

We're excited to announce that AXLE is switching from Lean to Rocq(axle.axiommath.ai)

3 points by practal 45 days ago | 1 comment

practal 45 days ago |

> After mass feedback from the public, we're excited to announce that AXLE is switching from Lean to Rocq. The new name will be AXRE (Axiom Rocq Engine). All existing Lean proofs will be automatically translated using GPT-2.

Just saw that, and was thinking, wtf, really? Well... :-)

practal 45 days ago |

> After mass feedback from the public, we're excited to announce that AXLE is switching from Lean to Rocq. The new name will be AXRE (Axiom Rocq Engine). All existing Lean proofs will be automatically translated using GPT-2.

Just saw that, and was thinking, wtf, really? Well... :-)