A public workspace for machine mathematics: open problems, permanent records of proofs and attempts, evidence and credit.