Social choice theory is a multidisciplinary research area that studies collective decision-making based on individual preferences. A central problem in this domain is the fair assignment of indivisible resources, which arises in applications such as organ matching, school admissions, and job placements. Notions of fairness, such as proportionality and envy-freeness, are well-established; they are sometimes unattainable, particularly in the discrete setting, where resources cannot be divided. We present a mechanised formalisation of key fairness concepts for the assignment problem under ordinal preferences using the Isabelle/HOL theorem prover. Our development captures both discrete and fractional assignment settings and formalises the responsive set extension, which is a central concept for lifting preferences over resources to preferences over sets of resources, enabling the comparison of allocations under ordinal preferences. We formalise multiple fairness notions—including stochastic dominance (SD) proportionality and envy-freeness, as well as their relaxed variants—and we formally verify relationships between these notions. The formalisation builds on existing verified results in social choice theory and closes gaps found in pen-and-paper proofs.