picrin

4 ms·

1. 1.▲
   by picrin 9y ago

   I'd say that using neural networks to solve sudoku-like puzzles is a bad idea -- a SAT solver, constraints program or integer program would be all quicker to run and quicker to implement.
2. 2.▲
   by picrin 10y ago

   Well, most of the work (asm.js compiler, github pages template) has been done by lean developers (and I agree, it's a marvel): https://github.com/leanprover/mkleanbook My contribution is just the content. There ar
3. 3.▲
   6 proofs of 2 + 2 = 2 * 2(lean-ide.github.io)

   3 points by picrin 10y ago|3 comments
4. 4.▲
   by picrin 10y ago

   Well, have a look at the two tutorials to which I link in readme.md of the github project. The first is very suitable for programmers with minimal prior knowledge of maths, the second is aimed at the opposite audience (mathematicians withou
5. 5.▲
   by picrin 10y ago

   By easier I mean there's a good tutorial and a low barrier of entry (you can learn to type proofs in the browser). When a couple years ago I decided to teach myself coq, I very quickly gave up, because there just wasn't any good e
6. 6.▲
   by picrin 10y ago

   Formal proofs are becoming easier. This proof was achieved in a couple days of intermittent effort, starting with no knowledge of formal proofs.
7. 7.▲
   Show HN: A formal proof of deMorgan's law in lean(github.com)

   3 points by picrin 10y ago|5 comments
8. 8.▲
   by picrin 10y ago

   What about adblock, adblock+? Is it possible for it to work as a webapp?