I will describe how the Lean proof assistant software can be used to teach mathematical reasoning to young students at university. This is different from teaching how to use Lean. Here Lean is only a tool, not the end goal.
I will explain what we can hope to teach using this tool, what are the available resources for teachers, and what choices should be made. I will then show my teaching library, Verbose Lean, which uses controlled natural language and customizable automation to optimize transfer of skills to paper proofs.
Refrigerators are inseparable from everyday life, industrial manufacturing, and research labs. In this talk, I will present our recent investigation on the refrigerator working between a finite-sized cold heat sink (which means that the heat capacity of the cold bath is finite) and an infinite-sized hot reservoir (environment). We assume that initially the finite-sized cold heat sink at temperature Ti ≤ Th, where Th is the hot reservoir temperature. By consuming the input work/power, the refrigerator transfers the heat from a finite-sized cold sink to the hot heat reservoir. Hence, the temperature of the finite-sized cold heat sink starts to decrease until it reaches the desired low-temperature Tf. By minimizing the input work in this heat transport process, we find the optimal path for temperature rate. We also calculate the coefficient of performance of the refrigerator.
