What might be the best software for checking the validity of proofs of graph theoretical statements? Lean, HOL, ... ? One criterion would also be, what would be the easiest for a graph theorist to learn and use, and what would allow the most economical (less time consuming) “programming”. Existing software has been used to check, for example, the validity of the proof of the four color theorem, but the issue here is, at this time and date, what would be best, taking into account the criteria that I mentioned above?

If MO is not the appropriate site for this question, please inform, I am only getting acquainted with what is proper and what is not for this site. I will automatically delete this question if downvotes arrive ...