News for hackers. Stuff that matters.

Show HN: I made PeanoScript, an educational TypeScript-like theorem prover

https://peanoscript.mjgrzymek.com/tutorial

Hi HN, I made this with the idea that many people are somewhat familiar with TypeScript and first-order logic, so combining them could be a nice introduction to automated theorem proving. My CS freshman logic class woefully lacked an interactive code environment

It's completely web-based so you can go ahead and try the interactive tutorial https://peanoscript.mjgrzymek.com/tutorial . Everything is explained on its own terms, so it should be readable if you just know programming.

If you already know this kind of stuff and want a tldr, there is also a reference https://peanoscript.mjgrzymek.com/reference and playground https://peanoscript.mjgrzymek.com/playground

The code is out on GitHub https://github.com/mjgrzymek/PeanoScript

Have fun!

( 1 comment | 2 points | on HN )
Re:Show HN: I made PeanoScript, an educational TypeScript-li... by MJGrzymek on Saturday March 22, 2025 @03:49PM (#43448132)
You can also see my post on reddit where I answer some questions https://www.reddit.com/r/ProgrammingLanguages/comments/1jfxj...