Reed's Conjecture for triangle-free graphs with maximum degree 6

### What is the conjecture

Reed's Conjecture in its general form is that the chromatic number of a graph is at most halfway between its trivial lower bound (clique number omega) and its trivial upper bound (maximum degree Delta, plus one), rounded up.

I suggest formalizing the simplest open case: Delta=6, omega=2, as described here:
https://mathoverflow.net/questions/37923/does-every-triangle-free-graph-with-maximum-degree-at-most-6-have-a-5-colouring

### Prerequisites needed

Let me take a crack at giving the conjecture in a slightly more formal language.

For any undirected graph G=(V,E) where V is a set of vertices and E is a set of undirected edges,

if for every v in V, the set of edges in E containing v has size at most 6, and

if for every v in V, there are no two other vertices u,w in V with the property that ( {v,u} in E and {v,w} in E and {u,w} in E )

then there is a function f:V->{1,2,3,4,5} such that for all {v,u} in E, f(v) != f(u).

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-05C15

### Choose either option
- [ ] I plan on working on this conjecture
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else