Skip to content

Instantly share code, notes, and snippets.

@alcides

alcides/stats.py

Last active October 18, 2022 08:23
Show Gist options
  • Save alcides/e71c3571527cb89b9cf722980860fda7 to your computer and use it in GitHub Desktop.
Save alcides/e71c3571527cb89b9cf722980860fda7 to your computer and use it in GitHub Desktop.
Download ZIP
Solution to Timothy Gowers's Daughter Homework
Raw
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]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment