Many 3-colorings of triangle-free planar graphs

Grِtzsch proved that every planar triangle-free graph is 3-colorable. We prove that it has at least 2 n 1 / 12 / 20 000 distinct 3-colorings where n is the number of vertices. If the graph has girth at least 5, then it has at least 2 n / 10 000 distinct list-colorings provided every vertex has at least three available colors.