Show HN: i2forge – A Platform for Verified Reasoning

&gt; It occupies the place of Peano&#x27;s * first axiom that 1 ∈ N. *&#x2F;<p>Natural numbers should start with 0 [0].<p>Suspiciously, the following lines in the proof can be entirely removed while still verifying:<p><pre><code> @func nat(x any) bool; term 1 nat; </code></pre> [0] <a href="https:&#x2F;&#x2F;www.cs.utexas.edu&#x2F;users&#x2F;EWD&#x2F;transcriptions&#x2F;EWD08xx&#x2F;EWD831.html" rel="nofollow">https:&#x2F;&#x2F;www.cs.utexas.edu&#x2F;users&#x2F;EWD&#x2F;transcriptions&#x2F;EWD08xx&#x2F;E...</a>

Interesting project. How does i2 compare with other languages used in verification &#x2F; theorem proving, such as Agda, Lean, Isabelle, etc?<p>From your site:<p>&gt; i2forge is a commercial venture, unlike i2<p>How are you planning to monetize i2forge?

I like the way you are thinking about this. And yes, formal math is the future! If you want to check out how to deal with quantification properly, or more generally with operators, without a need to explicitly introduce types, check out <a href="https:&#x2F;&#x2F;practal.com" rel="nofollow">https:&#x2F;&#x2F;practal.com</a> .