Curious about computer-assisted NP-completeness proofs
As for question 2, there are at least two examples of $NP$-completeness proofs that involve computer-assistant.

Erickson and  Ruskey provided a computer-aided proof that Domino Tatami Covering is NP-complete. They gave a polynomial time reduction from planar 3-SAT to tatami domino covering. A SAT-solver (Minisat) was used to automate gadgets discovery in the reduction. No other $NP$-completeness proof is known for it.

Ruepp and Holzer proved that pencil puzzle Kakuro is $NP$-complete. Some parts of the $NP$-completeness proof were generated automatically using a SAT-solver ( again Minisat).