Solution to Timothy Gowers's Daughter Homework

stats.py

# Puzzle from: https://twitter.com/wtgowers/status/1581667648592826369?s=12&t=5CR5L4TsH2MJWDJwBO8Wmw

import z3
s = z3.Solver()
a, b, c, d, e = z3.Ints("a b c d e")

# order
s.add( a <= c  )
s.add( b <= c  )
s.add( c <= d  )
s.add( c <= e  )
s.add( a <= b  )
s.add( d <= e  )

# Mean
s.add( (a + b + c + d + e) / 5 == 20  )

# Median
s.add(c == 21)

# Mode
s.add( d == 24)
s.add( e == 24)

# Check if there is a solution:
s.check() # returns sat

# Ask for the solution
print(s.model()) 
# Returns [b = 20, d = 24, c = 20, e = 24, a = 12]