In this work, new definitions of hypergraph products are presented. The main focus is on the generalization of the commutative standard graph products: the Cartesian, the direct and the strong graph product. We will generalize these well-known graph products to products of hypergraphs and show several properties like associativity, commutativity and distributivity w.r.t. the disjoint union of hypergraphs. Moreover, we show that all defined products of simple (hyper)graphs result in a simple (hyper)graph. We will see, for what kind of product the projections into the factors are (at least weak) homomorphisms and for which products there are similar connections between the hypergraph products as there are for graphs. Last, we give a new and more constructive proof for the uniqueness of prime factorization w.r.t. the Cartesian product than in [Studia Sci. Math. Hungar. 2: 285–290 (1967)] and moreover, a product relation according to such a decomposition. That might help to find efficient algorithms for the decomposition of hypergraphs w.r.t. the Cartesian product.

This study aimed to investigate the level of understanding of Euclidian geometry, in terms of theoretical knowledge as well as its problem-solving application, in pre-service mathematics education (PME) students at the University of Pretoria. In order to do so, a one group pre-test/ post-test procedure was conducted around an intensive geometry module, and a representational group of students was interviewed before and after the module to discuss their high school experiences of learning geometry and to analyse their attitudes towards the subject. The van Hiele Theory of Levels of Thought in Geometry was used as the theoretical framework for this study. The PME students in this study, prior to their completion of the geometry module, lacked the content knowledge, skills and insight in Euclidian geometry that is expected at matric level (Level 3). The pre-test results revealed that half the group could only be classified as being on Level 0. By the time the post-test was written, 60% of the group had moved onto Level 1 as their maximum competence level. This implies that these students were all brought to greater insight by the teaching they received during the geometry module. However, the overall improvement in the group as revealed in the post-test results, consisted of an upward movement of only one level. Therefore, the geometry module offered did not bring about sufficient improvement for these students to be able to teach geometry adequately (Level 3 is required). The students who were interviewed for this study uniformly expressed their dislike or fear of Euclidian geometry in general, but described the positive change in their attitude during the course of the module because of the way it was presented. Training of students for a career as mathematics educators which includes an in-depth van Hiele-based geometry module would facilitate the acquisition of insight and relational understanding. / Dissertation (MEd)--University of Pretoria, 2008. / Curriculum Studies / MEd / unrestricted

This study examines how formal mathematics can be taught in the Swedish secondary school with its new curriculum for mathematics. The study examines what a teaching material in formal mathematics corresponding to the initial content of the course Mathematics 1c could look like, and whether formal mathematics can be taught to high school students. The survey was conducted with second year students from the science programme. The majority of these students studied the course Mathematics D. The students described themselves as not being motivated towards mathematics. The results show that the content of the curriculum can be presented with formal mathematics. This both in terms of requirements for content and students being able to comprehend this content. The curriculum also requires that this type of mathematics is introduced in the course Mathematics 1c. The results also show that students are open towards and want more formal mathematics in their ordinary education. They initially felt it was strange because they had never encountered this type of mathematics before, but some students found the formal mathematics to be easier than the mathematics ordinarily presented in class. The study finds no reason to postpone the meeting with the formal mathematics to university level. Students’ commitment to proof and their comprehention of content suggests that formal mathematics can be introduced in high school courses. This study thus concludes that the new secondary school course Mathematics 1c can be formalised and therefore makes possible a renewed mathematics education. / Denna studie undersöker hur formell matematik kan undervisas i den nya svenska gymnasieskolan med dess nya ämnesplan för matematik. I studien undersöks hur ett undervisningsmaterial i formell matematik motsvarande det inledandeinnehållet i kursen Matematik 1c kan se ut och huruvida denna matematik kan undervisas med gymnasieelever. Undersökningen genomfördes med elever från det naturvetenskapliga programmets andra årskurs. Majoriteten av dessa elever läste då kursen Matematik D. Eleverna beskrev sig själva som ej motiverade i matematik. Resultatet visar att innehållet i ämnesplanen kan presenteras med formell matematik. Detta både med avseende ämnesplanens krav på innehåll och atteleverna kan förstå innehållet. Ämnesplanen kräver dessutom att denna typ av matematik tas upp som en del av innehållet i kursen Matematik 1c. Resultatet visar också att eleverna är öppna för och vill ha mer formell matematik i undervisningen. De tyckte att det kändes ovant eftersom att de aldrig tidigare stött på denna typ av matematik, men vissa elever fann formell matematik som enklare än matematiken som normalt presenteras på lektionerna. Studien finner ingen anledning till att skjuta upp mötet med formell matematik till universitetsnivå. Elevernas engagemang för bevis och tillgodogörandet av innehållet talar också för att formell matematik kan introduceras i gymnasiekurserna. Studiens slutsats är således att nya gymnasieskolans kurs Matematik 1c kan formaliseras och öppna för en förnyad matematikundervisning.

A trans man struggles to stay euphoric on his first day on testosterone in a world where his anxieties and emotional baggage talk back to him. He realizes becoming a self-made man comes with self-made problems. PW for Vimeo Link: DianaSeason2022!

No description available.

Information retrieval within a company can be referred to as enterprise search. With the use of enterprise search, employees can find the information they need in company internal data. If a business can take advantage of the knowledge within the organization, it can save time and effort, and be a source for innovation and development within the company.  In this project, two open source search engines, Recoll and Apache Solr, are selected, set up, and evaluated based on requirements and needs at the pharmacometric consulting company Pharmetheus AB. A requirement analysis is performed to collect system requirements at the company. Through a literature survey, two candidate search engines are selected. Lastly, a Proof of Concept is performed to demonstrate the feasibility of the search engines at the company. The search tools are evaluated on criteria including indexing performance, search functionality and configurability. This thesis presents assessment questions to be used when evaluating a search tool. It is shown that the indexing time for both Recoll and Apache Solr appears to scale linearly for less than one hundred thousand pdf documents. The benefit of an index is demonstrated when search times for both search engines greatly outperforms the Linux command-line tools grep and find. It is also explained how the strict folder structure and naming conventions at the company can be used in Recoll to only index specific documents and sub-parts of a file share. Furthermore, I demonstrate how the Recoll web GUI can be modified to include functionality for filtering on document type.  The results show that Recoll meets most of the company’s system requirements and for that reason it could serve as an enterprise search engine at the company. However, the search engine lacks support for authentication, something that has to be further investigated and implemented before the system can be put into production.

Dedukti est un cadre logique résultant de la combinaison du typage dépendant et de la réécriture. Il permet d'encoder de nombreux systèmes logiques au moyen de plongements superficiels qui préservent la notion de réduction. Ces traductions de systèmes logiques dans un format commun sont une première étape nécessaire à l'échange de preuves entre ces systèmes. Cet objectif d'interopérabilité des systèmes de preuve est la motivation principale de cette thèse. Pour y parvenir, nous nous inspirons du monde des langages de programmation et plus particulièrement des langages orientés-objet parce qu'ils mettent en œuvre des mécanismes avancés d'encapsulation, de modularité et de définitions par défaut. Pour cette raison, nous commençons par une traduction superficielle d'un calcul orienté-objet en Dedukti. L'aspect le plus intéressant de cette traduction est le traitement du sous-typage. Malheureusement, ce calcul orienté-objet ne semble pas adapté à l'incorporation de traits logiques. Afin de continuer, nous devons restreindre les mécanismes orientés-objet à des mécanismes statiques, plus faciles à combiner avec la logique et apparemment suffisant pour notre objectif d'interopérabilité. Une telle combinaison de mécanismes orientés-objet et de logique est présente dans l'environnement FoCaLiZe donc nous proposons un encodage superficiel de FoCaLiZe dans Dedukti. Les difficultés principales proviennent de l'intégration de Zenon, le prouveur automatique de théorèmes sur lequel FoCaLiZe repose, et de la traduction du langage d'implantation fonctionnel de FoCaLiZe qui présente deux constructions qui n'ont pas de correspondance simple en Dedukti : le filtrage de motif local et la récursivité. Nous démontrons finalement comment notre encodage de FoCaLiZe dans Dedukti peut servir en pratique à l'interopérabilité entre des systèmes de preuve à l'aide de FoCaLiZe, Zenon et Dedukti. Pour éviter de trop renforcer la théorie dans laquelle la preuve finale est obtenue, nous proposons d'utiliser Dedukti en tant que méta-langage pour éliminer des axiomes superflus. / Dedukti is a Logical Framework resulting from the combination ofdependent typing and rewriting. It can be used to encode many logical systems using shallow embeddings preserving their notion of reduction. These translations of logical systems in a common format are a necessary first step for exchanging proofs between systems. This objective of interoperability of proof systems is the main motivation of this thesis.To achieve it, we take inspiration from the world of programming languages and more specifically from object-oriented languages because they feature advanced mechanisms for encapsulation, modularity, and default definitions. For this reason we start by a shallow translation of an object calculus to Dedukti. The most interesting point in this translation is the treatment of subtyping. Unfortunately, it seems very hard to incorporate logic in this object calculus. To proceed, object-oriented mechanisms should be restricted to static ones which seem enough for interoperability. Such a combination of static object-oriented mechanisms and logic is already present in the FoCaLiZe environment so we propose a shallow embedding of FoCaLiZe in Dedukti. The main difficulties arise from the integration of FoCaLiZe automatic theorem prover Zenon and from the translation of FoCaLiZe functional implementation language featuring two constructs which have no simple counterparts in Dedukti: local pattern matching and recursion. We then demonstrate how this embedding of FoCaLiZe to Dedukti can be used in practice for achieving interoperability of proof systems through FoCaLiZe, Zenon, and Dedukti. In order to avoid strengthening to much the theory in which the final proof is expressed, we use Dedukti as a meta-language for eliminating unnecessary axioms.

Si l’étude du formalisme et du consensualisme peut constituer un thème classique du droit français, une confrontation de ces grandes notions du droit privé avec l’électronique est moins commune. Pourtant, la transmission électronique des volontés invite à réfléchir au défi lancé aux principes classiques de formation du contrat. Défi partiellement relevé par le législateur qui, en raison de l’abolition du support papier, a dû harmoniser ces notions. Manifestées par des formes libres ou imposées, les volontés devaient pouvoir circuler en ligne. Sans que le consensualisme ne soit explicitement visé, la rencontre de l’offre avec l’acceptation a été adaptée aux contraintes électroniques. Toutefois, il en résulte une réglementation souffrant d’une terminologie et d’un régime imprécis. Pour l’offre, la profusion du formalisme informatif, sans sanction, et le déni de sa forme écrite sont particulièrement incommodants. Pour l’acceptation, la portée du double-clic ou de l’accusé de réception sont encore incertaines. Concernant le formalisme, la transposition de l’acte sous signature privée et de l’acte authentique a inévitablement contribué à la dénaturation de ces formes. Pour le premier, les traits sont alourdis : comment des mentions manuscrites, supposant un irrémédiable lien physique entre la main de l’auteur et l’écriture, pouvaient-elles se réaliser en ligne sans une consolidation technique ? Pour le second, paradoxalement, son avenir semble conditionné par l’assouplissement du caractère mystique de l’authenticité, pour laisser place à une nouvelle authenticité électronique. D’où la nécessité de perfectionner l’adaptation des notions.Cette dernière fait en réalité surgir un mouvement plus profond. Une fois transposés à l’électronique, le consensualisme et le formalisme paraissent infidèles à leurs conceptions traditionnelles. Aussi, les notions seraient-elles exposées à une véritable transformation. Ce qui ne peut être neutre en droit commun des contrats. Concernant le consensualisme, la hiérarchie créée entre les formes et la discrimination des formes non-électroniques suggèrent un renouvellement de son approche classique. L’élaboration d’un néo-consensualisme est envisagée, faisant apparaître une nouvelle dualité du consensualisme en droit commun. Quant aux formalismes ad validitatem et ad probationem, l’impact de l’électronique se concentre sur leurs rapports mutuels. En ligne, leur dissociation devient impossible. Outre une assimilation textuelle, il y aurait une fusion substantielle des écrits, quel que soit leur rôle juridique. Or, une telle union ravive les couleurs d’un phénomène d’unification connu en droit commun des contrats. Il n’y a, alors, qu’un pas vers l’unité du formalisme.Loin d’une abolition des notions, leur mise à l’épreuve par l’électronique invite finalement à repenser les principes de la formation du contrat. / If the study of formalism and consensualism can constitute a classical theme of French law, a comparison of these great notions of private law with electronics is less common. However, the electronic transmission of wills invites to think about the challenge to the conventional principles of contract formation. A challenge partially raised by the legislator who, because of the abolition of paper support, had to adapt these notions. Wills, expressed by free or imposed forms, had to be able to circulate online. Without consensualism being explicitly targeted, the meeting of supply with acceptance has been adapted to electronic constraints. Nevertheless, the result is a regulation with an unclear terminology and regime. For the offer, the profusion of informative formalism, without sanction, and the denial of its written form are particularly bothersome. For acceptance, the scope of the double-click, or the acknowledgment of receipt, are still uncertain. Concerning formalism, the transposition of the act under private signature and the authentic act inevitably contributed to the denaturation of these forms. For the first, the traits are weighed down: how could handwritten mentions, assuming an irremediable physical link between the author's hand and the writing, be realized online without a technical consolidation? For the second, paradoxically, its future seems conditioned by the relaxation of the mystical character of authenticity, to give way to a new electronic authenticity. Hence the need to perfect the adaptation of notions.It actually causes a deeper movement. Once transposed to electronics, consensualism and formalism seem unfaithful to their traditional conceptions. Also, the notions would be exposed to a real transformation. This can not be neutral in common law contracts. Concerning consensualism, the hierarchy created between forms and the discrimination of non-electronic forms suggest a renewal of its classical approach. The development of a neo-consensualism is envisaged, bringing out a new duality of consensualism in common law. As for the formalisms ad validitatem and ad probationem, the impact of the electronics focuses on their mutual relations. Online, their dissociation becomes impossible. In addition to a textual assimilation, there would be a substantial fusion between the writings, whatever their legal role. However, such a union revives the colors of a unifying phenomenon known in the common law of contracts. There is then only one step towards the unity of formalism.Far from an abolition of notions, their testing by the electronics finally invites to rethink the principles of the formation of the contract.

Cette recherche porte sur les médecins légistes et les expertises qu’ils effectuent sur réquisitions du procureur. Ni collaborateurs occasionnels du juge, ni détenteurs d’un titre de spécialité spécifique, les médecins légistes constituent un corps professionnel à distance à la fois du modèle de l’expertise judiciaire et de celui des spécialités médicales. Ils exercent l’expertise médico-légale à titre principal dans des services hospitaliers dédiés, après avoir suivi un cursus dans une spécialité médicale allant de la médecine générale à l’anatomopathologie, en passant par la médecine du travail et la santé publique.La thèse explore la tension entre expertise judiciaire et spécialité médicale et l’analyse simultanément comme étant inscrite dans le processus de constitution du groupe professionnel des médecins légistes, et comme résidant au cœur d’activités de coproduction des vérités médicale et judiciaire sur les faits. Cette recherche repose sur la mise en place d’un dispositif d’enquête empirique associant des observations ethnographiques, des entretiens et un travail documentaire. Les différents sites étudiés (salles d’autopsies, cabinets médicaux, directions ministérielles, administrations déconcentrées, permanences-parquet, cours d’assises, congrès de médecine légale) sont constitutifs du dispositif médico-légal étudié selon deux plans distincts : le plan des protocoles qui, des ministères aux services, vise à organiser et cadrer les activités médico-légales ; celui des rapports d’expertise établis par les médecins légistes, qu’il s’est agi de suivre depuis les services de médecine légale jusqu’aux tribunaux. La première partie consiste à explorer le plan des protocoles, en étudiant notamment la genèse, l’élaboration et la mise en œuvre d’une réforme de la médecine légale. Elle montre que l’organisation des activités médico-légales a oscillé entre deux définitions de l’expertise médico-légale qui instituent respectivement une figure du médecin expert judiciaire et une figure du légiste spécialiste. La deuxième partie retrace les carrières de ceux qui s’engagent dans l’expertise médico-légale. Elle montre que les postures des médecins vis-à-vis de l’expertise médico-légale dépendent de la façon dont ils ajustent l’exercice de cette activité à leur formation médicale d’origine. Enfin, la troisième partie traite des pratiques des experts et des magistrats du parquet, au sein des organisations où les expertises médico-légales sont produites et utilisées, de l’hôpital au tribunal. Cette ethnographie de l’élaboration des preuves médico-légales révèle les tensions qui apparaissent dans le flux de l’activité du fait des différents cadres que les médecins associent dans leurs explorations des corps violentés.Cette approche mobile du dispositif médico-légal permet de soulever deux enjeux théoriques. D’abord, l’articulation entre le niveau micro des pratiques et le niveau méso des organisations conduit à renouveler l’approche par les segments professionnels. L’étude des processus de segmentation permet ici de déterminer si la médecine légale est une activité pilotée depuis la tutelle judiciaire qui finance et consomme des rapports d’expertise, ou si elle tend à devenir une discipline médicale autonome régulée comme une spécialité depuis l’hôpital. Le deuxième enjeu consiste à étudier les processus de socialisation au dispositif et les pratiques des experts de façon dynamique. En définitive, cette thèse propose d’analyser une pratique tendue entre différents cadres mobilisés en situation, tout en analysant certains déterminants sociaux du jugement médico-légal par l’exploration dynamique de trois échelles distinctes : l’organisation de la médecine légale, la socialisation des médecins légistes et l’activité des professionnels qui produisent et se saisissent des rapports médico-légaux. / This research focuses on medical examiners and the reports they provide upon requisition from Public Prosecutors. Neither occasional collaborators of the judge, nor holders of a specific specialty title, forensic scientists and medical examiners form a professional body that is quite distant from both the judicial expert assessment model and the medical specialty model. They mainly practise the medico-legal expertise in dedicated hospital units, and have undergone a medical university curriculum, with medical specialties ranging from general medicine to anatomopathology, and from occupational medicine to public health.This thesis explores the tension between a judicial expert assessment and a medical specialty, and analyses this tension, simultaneously as being enshrined into the formation process of the occupational group, and as a driving force of the coproduction of medical and judicial truths about facts. The research builds on the implementation of an empirical investigation system, associating ethnographic observations, interviews, and documentation. The different locations that were analysed (autopsy rooms, doctors’ offices, Ministerial directions, decentralised administrations, Public Prosecutors’ committee rooms, congress) constitute a two-level analysis of the medico-legal apparatus: on one hand, the protocol level, where medico-legal activities are organised and supervised, from state-level administrations to local departments; on the other hand, the expert assessment level, where medical examiners were studied from medical examination rooms up to courts of law. The first chapter explores the protocol level, by studying, in particular, the genesis, elaboration and implementation of a forensic medicine reform. It highlights how the organisation of medico-legal activities has been oscillating between two definitions of a medico-legal expertise; these two definitions respectively establish the figure of a judicial expert doctor, and the figure of a forensic specialist. The second chapter focuses on the careers of those who embrace the medico-legal expertise field. It reveals how doctors’ positions on medico-legal expertise are reliant on the way they adjust the practising of this activity to their original medical education. Finally, the third chapter analyses the practices of experts and magistrates from the Public Prosecutor’s department, within the organisations where the medico-legal expert assessments are produced and used, from hospitals to courts of law. This ethnography of how medico-legal evidence is created underlines the tensions that come up within this activity stream, as doctors mix up different frameworks in the way they examine assaulted bodies.This mobile approach of the medico-legal apparatus allows the surfacing of two theoretical concerns. First, the logical hierarchy between the micro level of practises and the meso level of organisations leads to renew the approach for professional segments. Studying segmentation processes is a way of determining if forensic medicine is more driven towards being an activity that is piloted by the judicial administration supervision (which funds and consumes the expert assessments), or towards becoming an autonomous medical discipline with the same regulation mechanisms as a regular hospital specialty. This second concern leads to studying the socialization mechanism as well as the practises of experts in a dynamic way. Ultimately, this thesis proposes to analyse a practise that is stretched between different surroundings in concrete situations, while analysing specific social determining factors of the medico-legal assessment, by dynamically exploring three levels: the organisation of forensic medicine, the socialization of the experts, and the actual activity of the professionals that produce and seize medico-legal assessments.

Cette thèse propose trois contributions aux preuves mathématiques assistées par ordinateur. On s'intéresse non seulement aux preuves reposant sur le calcul, mais aussi aux preuves formelles, qui sont àla fois produites et vérifiées à l'aide d'un logiciel appelé assistant à la preuve.Dans la première partie, nous illustrons le thème de l'expérimentation au service de la preuve en nous intéressant au problème de la complexité des algorithmes de multiplication matricielle. Cette question a historiquement été posée de manière de plus en plus abstraite: les approches modernes ne construisent pas d'algorithmes explicites mais utilisent des résultats théoriques pour améliorer la borne inférieure sur la célèbre constante oméga. Nous sommes revenus à une approche plus pratique en essayant de programmer certains des algorithmes impliqués par ces résultats théoriques. Cette approche expérimentale a révélé un motif inattendu dans des algorithmes existants. Alors que ces algorithmes contiennent une nouvelle variable epsilon dont la présence est réputée les rendre impraticables pour des tailles de matrices raisonnables, nous avons découvert que nous pouvions construire des algorithmes de multiplication matricielle en parallèle sans epsilon avec une complexité asymptotique qui peut théoriquement battre l'algorithme de Strassen pour les multiplications. Un sous-produit de cette exploration est un outil symbolique en Ocaml qui peut analyser, composer et exporter des algorithmes de multiplication matricielle. Nous pensons aussi qu'il pourrait être utilisé pour construire de nouveaux algorithmes pratiques de multiplication matricielle.Dans la deuxième partie, nous décrivons une preuve formelle de l'irrationalité de la constante zeta(3), en suivant la démonstration historique due à Apéry. L'étape cruciale de cette preuve est d'établir que deux suites de nombres rationnels satisfont une surprenante récurrence commune. Il est en fait possible de "découvrir"cette récurrence en utilisant des algorithmes symboliques, et leurs implémentations existantes dans un système de calcul formel. De fait,ce travail constitue un exemple d'une approche dite sceptique de la démonstration formelle de théorèmes, dans lequel des calculs sont principalement réalisés par un logiciel efficace de calcul formel puis vérifiés formellement dans un assistant à la preuve. Incidemment, ce travail questionne la valeur des certificats de télescopage créatif comme preuves complètes d'identités. Cette preuve formelle est également basée sur de nouvelles bibliothèques de mathématiques,formalisées pour ses besoins. En particulier, nous avons formalisé et simplifié une étude du comportement asymptotique de la suite ppcm(1,.., n). Ce travail est conduit dans l'assistant à la preuve Coq et prolonge les bibliothèques Mathematical Components.Dans la dernière partie, nous présentons une procédure qui calcule les approximations d'une classe d'intégrales propres et impropres tout en produisant simultanément un preuve formelle Coq de la correction du résultat de ce calcul. Cette procédure utilise une combinaison d'arithmétique d'intervalles et d'approximations polynomiales rigoureuses de fonctions. Ce travail utilise crucialement les possibilités de calculer efficacement à l'intérieur de la logique sous-jacente au système Coq. Il s'agit d'une extension de la bibliothèque CoqInterval d'approximation numérique d'une classe d'expressions réelles. Sa mise en œuvre a également donné lieu à des extensions de la bibliothèque Coquelicot d'analyse réelle, notamment pour améliorer le traitement des intégrales impropres. Nous illustrons l'intérêt de cet outil et ses performances en traitant des exemples standards mais non triviaux de la littérature, sur lesquels d'autres outils se sont en certains cas révélés incorrects. / This thesis proposes three contributions to computer-aidedmathematical proofs. It deals, not only with proofs relying oncomputations, but also with formal proofs, which are both produced andverified using a piece of software called a proof assistant.In the first part, we illustrate the theme of experimentation at theservice of proofs by considering the problem of the complexity ofmatrix multiplication algorithms. This problem has historically beenapproached in an increasingly abstract way: modern approaches do notconstruct algorithms but use theoretical results to improve the lowerbound on the famous omega constant. We went back to a more practicalapproach by attempting to program some of the algorithms implied bythese theoretical results. This experimental approach reveals anunexpected pattern in some existing algorithms. While these algorithmscontain a new variable epsilon whose presence is reputed to renderthem inefficient for the purposes of reasonable matrix sizes, we havediscovered that we could build matrix multiplication algorithms inparallel without epsilon's with an asymptotic complexity which cantheoretically beat Strassen's algorithm in terms of the number ofmultiplications. A by-product of this exploration is a symbolic toolin Ocaml which can analyze, compose and export matrix multiplicationalgorithms. We also believe that it could be used to build newpractical algorithms for matrix multiplication.In the second part, we describe a formal proof of the irrationality ofthe constant zeta (3), following the historical demonstration due toApéry. The crucial step of this proof is to establish that twosequences of rational numbers satisfy a suprising commonrecurrence. It is in fact possible to "discover" this recurrence usingsymbolic algorithms, and their existing implementations in a computeralgebra system. In fact, this work is an example of a skepticalapproach to the formal proof of theorems, in which computations aremainly accomplished by an efficient computer algebra program, and thenformally verified in a proof assistant. Incidentally, this workquestions the value of creative telescoping certificates as completeproofs of identities. This formal proof is also based on newmathematical libraries, which were formalised for its needs. Inparticular, we have formalized and simplified a study of theasymptotic behaviour of the sequence lcm(1,..., n). This work isdeveloped in the Coq proof assistant and extends the MathematicalComponents libraries.In the last part, we present a procedure which computes approximationsof a class of proper and improper integrals while simultaneouslyproducing a Coq formal proof of the correction of the result of thiscomputation. This procedure uses a combination of interval arithmeticand rigorous polynomial approximations of functions. This work makescrucial use of the possibility to efficiently compute inside Coq'slogic. It is an extension of the CoqInterval library providingnumerical approximation of a class of real expressions. Itsimplementation has also resulted in extensions to the Coquelicotlibrary for real analysis, including a better treatment of improperintegrals. We illustrate the value of this tool and its performanceby dealing with standard but nontrivial examples from the literature,on which other tools have in some cases been incorrect.