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.
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 are alternative tutorials available, but they all require significant time investment (weeks to months)