12 maart 2024
Het nadenken over nieuwe vraagstukken en de daaropvolgende uitdaging om daar iets aan bij te dragen. Hier komen steeds andere bezigheden bij kijken, van het opschrijven van nieuwe inzichten tot het oplossen van een wiskundig probleem. En van nieuwe algoritmes programmeren tot het leren over nieuwe gebieden binnen de wiskunde. Ook het lesgeven is een interessant onderdeel van deze bezigheden.
Dat is met stipt het onderzoek dat het eerste hoofdstuk van mijn proefschrift moet worden. De focus van dit project is het (numeriek) oplossen van optimale stopproblemen waarbij de stopmogelijkheden zich stochastisch en afhankelijk aandoen. Stopproblemen zijn problemen waarbij we een beslissing moeten maken om te stoppen, waarna we een uitbetaling ontvangen. Het doel hierbij is om het juiste moment te vinden waarop we willen stoppen, zodat de uitbetaling maximaal is. Een erg interessant vraagstuk, waarover we onlangs een preprint hebben uitgebracht.
2 van mijn hobby’s zijn het spelen van bordspellen en het formaliseren van wiskundige bewijzen. Dat laatste verdient waarschijnlijk wat toelichting. Formaliseren houdt in dat wiskundige bewijzen op een programmatische wijze aan een computer worden aangeboden, op zodanige wijze dat de computer kan verifiëren dat het bewijs logisch sluitend, en dus correct, is. Hiervoor werk ik mee aan de Mathlib bibliotheek van wiskundige definities en stellingen in Lean. Lean is een populaire programmeertaal voor dit doeleinde. Het is bijvoorbeeld onlangs gebruikt voor het verifiëren van de bewijzen voor het Liquid Tensor Experiment.