Eris theorem proving environment updates with direct manipulation

round · x · 2026-08-21

Progress on Eris, an environment designed for direct manipulation theorem proving. The post demonstrates a simple logical deduction of P from the premise ((P ∧ Q) ∧ (R ∧ P)) using two ∧-eliminations.

Original post →

More from Research

Research channel →